===========================================================
                                      .___ __  __   
          _________________  __ __  __| _/|__|/  |_ 
         / ___\_` __ \__  \ |  |  \/ __ | | \\_  __\
        / /_/  >  | \// __ \|  |  / /_/ | |  ||  |  
        \___  /|__|  (____  /____/\____ | |__||__|  
       /_____/            \/           \/           
              grep rough audit - static analysis tool
                  v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401050-       For example, you could try to "not define undefined terms"
metamath-databases-0.0.0~20200715.git5b44899/set.mm:401051:       by creating definitions like ${ $d ` y x ` $. $d ` y ph ` $.
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401052-       df-iota $a ` |- ( E! x ph -> ( iota x ph ) = U. { x | ph } ) ` $. $}.
##############################################
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401894-       ` F/_ x A ` or ` F/ x ph ` ; here it is.
metamath-databases-0.0.0~20200715.git5b44899/set.mm:401895:       ` |- ` T[x, A] where ` $d x A `,
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401896-       and you wish to prove ` |- F/_ x A => |- ` T[x, A].
##############################################
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401950-       <li>The defined expression must not appear in any statement
metamath-databases-0.0.0~20200715.git5b44899/set.mm:401951:       between its syntax axiom ( ` $a wff ` ) and its definition,
metamath-databases-0.0.0~20200715.git5b44899/set.mm-401952-       and the defined expression must be not be used in its definiens.