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

Theorem 19.21v 1913
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 1814 via the use of distinct variable conditions combined with nfv 1629. 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 2286 derived from df-eu 2284. 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 1629 . 2  |-  F/ x ph
2119.21 1814 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549
This theorem is referenced by:  pm11.53  1916  19.12vv  1921  cbval2  1989  sbhb  2182  2sb6  2188  sbcom2  2189  2sb6rf  2194  2exsb  2208  r3al  2750  ceqsralt  2966  euind  3108  reu2  3109  reuind  3124  unissb  4032  dfiin2g  4111  axrep5  4312  asymref  5236  dff13  5990  mpt22eqb  6165  findcard3  7336  marypha1lem  7424  marypha2lem3  7428  aceq1  7982  kmlem15  8028  dfon2lem8  25396  dffun10  25704  pm10.541  27472  pm10.542  27473  19.21vv  27484  pm11.62  27503  2sbc6g  27525  2rexsb  27857  bnj864  29045  bnj865  29046  bnj978  29072  bnj1176  29126  bnj1186  29128  sbhbwAUX7  29354  2sb6NEW7  29357  pm11.53OLD7  29430  19.12vvOLD7  29431  sbhbOLD7  29490  sbcom2OLD7  29491  2sb6rfOLD7  29493  2exsbOLD7  29498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator