MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21v Unicode version

Theorem 19.21v 1902
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  F/ x ph in 19.21 1804 via the use of distinct variable conditions combined with nfv 1626. 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 2237 derived from df-eu 2235. 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  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem 19.21v
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ x ph
2119.21 1804 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546
This theorem is referenced by:  pm11.53  1905  19.12vv  1910  sbhb  2133  2sb6  2139  sbcom2  2140  2sb6rf  2145  2exsb  2159  r3al  2699  ceqsralt  2915  euind  3057  reu2  3058  reuind  3073  unissb  3980  dfiin2g  4059  axrep5  4259  asymref  5183  dff13  5936  mpt22eqb  6111  findcard3  7279  marypha1lem  7366  marypha2lem3  7370  aceq1  7924  kmlem15  7970  dfon2lem8  25163  dffun10  25470  pm10.541  27224  pm10.542  27225  19.21vv  27236  pm11.62  27255  2sbc6g  27277  2rexsb  27609  bnj864  28624  bnj865  28625  bnj978  28651  bnj1176  28705  bnj1186  28707  sbhbwAUX7  28933  2sb6NEW7  28936  pm11.53OLD7  29009  19.12vvOLD7  29010  sbhbOLD7  29069  sbcom2OLD7  29070  2sb6rfOLD7  29072  2exsbOLD7  29077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator