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

Theorem 19.21v 2012
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 1771 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 2123 derived from df-eu 2121. 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 1771 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532
This theorem is referenced by:  pm11.53  2025  19.12vv  2032  sbhb  2070  2sb6  2076  sbcom2  2077  2sb6rf  2081  2exsb  2094  r3al  2571  ceqsralt  2762  euind  2903  reu2  2906  reuind  2917  unissb  3798  dfiin2g  3877  axrep5  4076  asymref  5012  fv2  5419  dff13  5682  mpt22eqb  5852  findcard3  7033  marypha1lem  7119  marypha2lem3  7123  aceq1  7677  kmlem15  7723  dfon2lem8  23480  pm10.541  26894  pm10.542  26895  19.21vv  26906  pm11.62  26925  2sbc6g  26948  bnj864  27966  bnj865  27967  bnj978  27993  bnj1176  28047  bnj1186  28049
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540
  Copyright terms: Public domain W3C validator