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

Theorem 19.21v 1785
Description: Version of 19.21 1986 with a dv condition.

Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as  F/ x ph. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1667) instead of a dv condition. For instance, 19.21v 1785 versus 19.21 1986 and vtoclf 3098 versus vtocl 3099. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1760. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.)

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 stdpc5v 1784 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
)
2 ax5e 1759 . . . 4  |-  ( E. x ph  ->  ph )
32imim1i 60 . . 3  |-  ( (
ph  ->  A. x ps )  ->  ( E. x ph  ->  A. x ps )
)
4 19.38 1711 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
53, 4syl 17 . 2  |-  ( (
ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
61, 5impbii 191 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1441   E.wex 1662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-ex 1663
This theorem is referenced by:  stdpc5vOLD  1787  19.32v  1788  pm11.53v  1821  19.12vvv  1822  pm11.53  2072  19.12vv  2075  cbval2  2119  sbhb  2266  2sb6  2272  r2al  2765  r3al  2767  r19.21v  2792  r3alOLD  2825  ceqsralt  3070  euind  3224  reu2  3225  reuind  3242  unissb  4228  dfiin2g  4310  axrep5  4519  asymref  5215  fvn0ssdmfun  6011  dff13  6157  mpt22eqb  6402  findcard3  7811  marypha1lem  7944  marypha2lem3  7948  aceq1  8545  kmlem15  8591  cotr2g  13033  bnj864  29726  bnj865  29727  bnj978  29753  bnj1176  29807  bnj1186  29809  dfon2lem8  30429  dffun10  30674  bj-ssb1  31239  bj-ssbcom3lem  31256  bj-cbval2v  31331  bj-axrep5  31400  bj-ralcom4  31470  mpt2bi123f  32399  mptbi12f  32403  elmapintrab  36176  undmrnresiss  36204  dfhe3  36364  dffrege115  36568  pm10.541  36710  pm10.542  36711  19.21vv  36719  pm11.62  36738  2sbc6g  36760  2rexsb  38585
  Copyright terms: Public domain W3C validator