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

Theorem 19.21v 1917
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 1817 via the use of distinct variable conditions combined with nfv 1631. 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 2294 derived from df-eu 2292. 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 1631 . 2  |-  F/ x ph
2119.21 1817 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550
This theorem is referenced by:  pm11.53  1920  19.12vv  1925  cbval2  1993  sbhb  2190  2sb6  2196  sbcom2  2197  2sb6rf  2202  2exsb  2216  r3al  2770  ceqsralt  2988  euind  3130  reu2  3131  reuind  3146  unissb  4074  dfiin2g  4154  axrep5  4356  asymref  5285  dff13  6040  mpt22eqb  6215  findcard3  7386  marypha1lem  7474  marypha2lem3  7478  aceq1  8036  kmlem15  8082  dfon2lem8  25452  dffun10  25794  mpt2bi123f  26790  mptbi12f  26794  pm10.541  27651  pm10.542  27652  19.21vv  27663  pm11.62  27682  2sbc6g  27704  2rexsb  28036  bnj864  29467  bnj865  29468  bnj978  29494  bnj1176  29548  bnj1186  29550  sbhbwAUX7  29781  2sb6NEW7  29784  sbcom2NEW7  29818  pm11.53OLD7  29874  19.12vvOLD7  29875  sbhbOLD7  29934  2sb6rfOLD7  29936  2exsbOLD7  29941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-11 1764
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator