New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  19.21v Unicode version

Theorem 19.21v 1890
 Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as in 19.21 1796 via the use of distinct variable conditions combined with nfv 1619. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2210 derived from df-eu 2208. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.21v
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem 19.21v
StepHypRef Expression
1 nfv 1619 . 2
2119.21 1796 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 176  wal 1540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545 This theorem is referenced by:  pm11.53  1893  19.12vv  1898  sbhb  2107  2sb6  2113  sbcom2  2114  2sb6rf  2118  2exsb  2132  r3al  2671  ceqsralt  2882  euind  3023  reu2  3024  reuind  3039  unissb  3921  dfiin2g  4000  ssfin  4470  spfininduct  4540  dff13  5471  spacind  6287
 Copyright terms: Public domain W3C validator