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

Theorem 19.21v 1843
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 1803 via the use of distinct variable conditions combined with nfv 1609. 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 2162 derived from df-eu 2160. 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 1609 . 2  |-  F/ x ph
2119.21 1803 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530
This theorem is referenced by:  pm11.53  1846  19.12vv  1851  sbhb  2059  2sb6  2065  sbcom2  2066  2sb6rf  2070  2exsb  2084  r3al  2613  ceqsralt  2824  euind  2965  reu2  2966  reuind  2981  unissb  3873  dfiin2g  3952  axrep5  4152  asymref  5075  dff13  5799  mpt22eqb  5969  findcard3  7116  marypha1lem  7202  marypha2lem3  7206  aceq1  7760  kmlem15  7806  dfon2lem8  24217  dffun10  24524  pm10.541  27665  pm10.542  27666  19.21vv  27677  pm11.62  27696  2sbc6g  27718  2rexsb  28051  bnj864  29270  bnj865  29271  bnj978  29297  bnj1176  29351  bnj1186  29353  sbhbwAUX7  29579  2sb6NEW7  29582  pm11.53OLD7  29654  19.12vvOLD7  29655  sbhbOLD7  29714  sbcom2OLD7  29715  2sb6rfOLD7  29718  2exsbOLD7  29723
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535
  Copyright terms: Public domain W3C validator