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 2124 derived from df-eu 2122. 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  2095  r3al  2575  ceqsralt  2786  euind  2927  reu2  2928  reuind  2943  unissb  3831  dfiin2g  3910  axrep5  4110  asymref  5047  fv2  5454  dff13  5717  mpt22eqb  5887  findcard3  7068  marypha1lem  7154  marypha2lem3  7158  aceq1  7712  kmlem15  7758  dfon2lem8  23515  pm10.541  26929  pm10.542  26930  19.21vv  26941  pm11.62  26960  2sbc6g  26983  bnj864  28003  bnj865  28004  bnj978  28030  bnj1176  28084  bnj1186  28086
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