NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  19.21v GIF 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 xφ 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 (x(φψ) ↔ (φxψ))
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem 19.21v
StepHypRef Expression
1 nfv 1619 . 2 xφ
2119.21 1796 1 (x(φψ) ↔ (φxψ))
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