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

Theorem 19.21v 1776
Description: Version of 19.21 1961 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 1665) instead of a dv condition. For instance, 19.21v 1776 versus 19.21 1961 and vtoclf 3133 versus vtocl 3134. 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 1752. 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 1775 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
)
2 ax5e 1751 . . . 4  |-  ( E. x ph  ->  ph )
32imim1i 61 . . 3  |-  ( (
ph  ->  A. x ps )  ->  ( E. x ph  ->  A. x ps )
)
4 19.38 1708 . . 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 1436   E.wex 1660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749
This theorem depends on definitions:  df-bi 189  df-ex 1661
This theorem is referenced by:  stdpc5vOLD  1778  19.32v  1779  pm11.53v  1812  19.12vvv  1813  pm11.53  2039  19.12vv  2042  cbval2  2082  sbhb  2234  2sb6  2240  r2al  2804  r3al  2806  r19.21v  2831  r3alOLD  2864  ceqsralt  3106  euind  3259  reu2  3260  reuind  3276  unissb  4248  dfiin2g  4330  axrep5  4539  asymref  5233  fvn0ssdmfun  6026  dff13  6172  mpt22eqb  6417  findcard3  7818  marypha1lem  7951  marypha2lem3  7955  aceq1  8550  kmlem15  8596  cotr2g  13034  bnj864  29735  bnj865  29736  bnj978  29762  bnj1176  29816  bnj1186  29818  dfon2lem8  30437  dffun10  30680  bj-cbval2v  31296  bj-axrep5  31371  bj-ralcom4  31441  mpt2bi123f  32326  mptbi12f  32330  dfhe3  36234  dffrege115  36438  pm10.541  36580  pm10.542  36581  19.21vv  36589  pm11.62  36608  2sbc6g  36630  2rexsb  38310
  Copyright terms: Public domain W3C validator