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

Theorem 19.21v 1754
Description: Version of 19.21 1935 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 1640) instead of a dv condition. For instance, 19.21v 1754 versus 19.21 1935 and vtoclf 3112 versus vtocl 3113. 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 1730. 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 1753 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
)
2 ax5e 1729 . . . 4  |-  ( E. x ph  ->  ph )
32imim1i 59 . . 3  |-  ( (
ph  ->  A. x ps )  ->  ( E. x ph  ->  A. x ps )
)
4 19.38 1685 . . 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 189 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186   A.wal 1405   E.wex 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727
This theorem depends on definitions:  df-bi 187  df-ex 1636
This theorem is referenced by:  stdpc5vOLD  1756  19.32v  1757  pm11.53v  1790  19.12vvv  1791  pm11.53  2013  19.12vv  2016  cbval2  2056  sbhb  2208  2sb6  2214  r2al  2784  r3al  2786  r19.21v  2811  r3alOLD  2844  ceqsralt  3085  euind  3238  reu2  3239  reuind  3255  unissb  4224  dfiin2g  4306  axrep5  4514  asymref  5206  fvn0ssdmfun  6002  dff13  6149  mpt22eqb  6394  findcard3  7799  marypha1lem  7929  marypha2lem3  7933  aceq1  8532  kmlem15  8578  cotr2g  12961  bnj864  29320  bnj865  29321  bnj978  29347  bnj1176  29401  bnj1186  29403  dfon2lem8  30022  dffun10  30265  bj-cbval2v  30879  bj-axrep5  30955  bj-ralcom4  31021  mpt2bi123f  31866  mptbi12f  31870  dfhe3  35768  dffrege115  35972  pm10.541  36133  pm10.542  36134  19.21vv  36142  pm11.62  36161  2sbc6g  36183  2rexsb  37556
  Copyright terms: Public domain W3C validator