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

Theorem 19.21v 1831
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 1791 via the use of distinct variable conditions combined with nfv 1605. 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 2149 derived from df-eu 2147. 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 1605 . 2  |-  F/ x ph
2119.21 1791 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527
This theorem is referenced by:  pm11.53  1834  19.12vv  1839  sbhb  2046  2sb6  2052  sbcom2  2053  2sb6rf  2057  2exsb  2071  r3al  2600  ceqsralt  2811  euind  2952  reu2  2953  reuind  2968  unissb  3857  dfiin2g  3936  axrep5  4136  asymref  5059  dff13  5783  mpt22eqb  5953  findcard3  7100  marypha1lem  7186  marypha2lem3  7190  aceq1  7744  kmlem15  7790  dfon2lem8  24146  dffun10  24453  pm10.541  27562  pm10.542  27563  19.21vv  27574  pm11.62  27593  2sbc6g  27615  2rexsb  27948  bnj864  28954  bnj865  28955  bnj978  28981  bnj1176  29035  bnj1186  29037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532
  Copyright terms: Public domain W3C validator