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

Theorem 19.21v 1842
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 1795 via the use of distinct variable conditions combined with nfv 1610. 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 2150 derived from df-eu 2148. 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 1610 . 2  |-  F/ x ph
2119.21 1795 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  1845  19.12vv  1850  sbhb  2041  2sb6  2050  sbcom2  2051  2sb6rf  2055  2exsb  2069  r3al  2601  ceqsralt  2812  euind  2953  reu2  2954  reuind  2969  unissb  3858  dfiin2g  3937  axrep5  4137  asymref  5058  fv2  5481  dff13  5744  mpt22eqb  5914  findcard3  7095  marypha1lem  7181  marypha2lem3  7185  aceq1  7739  kmlem15  7785  dfon2lem8  23547  pm10.541  26961  pm10.542  26962  19.21vv  26973  pm11.62  26992  2sbc6g  27014  2rexsb  27327  bnj864  28221  bnj865  28222  bnj978  28248  bnj1176  28302  bnj1186  28304
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1537
  Copyright terms: Public domain W3C validator