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 1794
Description: Version of 19.21 2007 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 1676) instead of a dv condition. For instance, 19.21v 1794 versus 19.21 2007 and vtoclf 3085 versus vtocl 3086. 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 1769. 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 1793 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
)
2 ax5e 1768 . . . 4  |-  ( E. x ph  ->  ph )
32imim1i 59 . . 3  |-  ( (
ph  ->  A. x ps )  ->  ( E. x ph  ->  A. x ps )
)
4 19.38 1720 . . 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 192 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1450   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  stdpc5vOLD  1796  19.32v  1797  pm11.53v  1830  19.12vvv  1831  pm11.53  2090  19.12vv  2091  cbval2  2133  sbhb  2287  2sb6  2293  r2al  2783  r3al  2784  r19.21v  2803  ceqsralt  3057  euind  3213  reu2  3214  reuind  3231  unissb  4221  dfiin2g  4302  axrep5  4513  asymref  5222  fvn0ssdmfun  6028  dff13  6177  mpt22eqb  6424  findcard3  7832  marypha1lem  7965  marypha2lem3  7969  aceq1  8566  kmlem15  8612  cotr2g  13115  bnj864  29805  bnj865  29806  bnj978  29832  bnj1176  29886  bnj1186  29888  dfon2lem8  30507  dffun10  30752  bj-ssb1  31310  bj-ssbcom3lem  31327  bj-cbval2v  31404  bj-axrep5  31473  bj-ralcom4  31545  mpt2bi123f  32470  mptbi12f  32474  elmapintrab  36253  undmrnresiss  36281  dfhe3  36441  dffrege115  36645  pm10.541  36786  pm10.542  36787  19.21vv  36795  pm11.62  36814  2sbc6g  36836  2rexsb  38736
  Copyright terms: Public domain W3C validator