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

Theorem 19.21v 2011
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 2120 derived from df-eu 2118. 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  2024  19.12vv  2031  sbhb  2067  2sb6  2073  sbcom2  2074  2sb6rf  2078  2exsb  2091  r3al  2562  ceqsralt  2749  euind  2889  reu2  2892  reuind  2903  unissb  3755  dfiin2g  3834  axrep5  4033  asymref  4966  fv2  5373  dff13  5635  mpt22eqb  5805  findcard3  6985  marypha1lem  7070  marypha2lem3  7074  aceq1  7628  kmlem15  7674  dfon2lem8  23314  pm10.541  26728  pm10.542  26729  19.21vv  26740  pm11.62  26759  2sbc6g  26782  bnj864  27643  bnj865  27644  bnj978  27670  bnj1176  27724  bnj1186  27726
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