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

Theorem 19.41v 1946
Description: Version of 19.41 2224 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1964. (Revised by Rohan Ridenour, 15-Apr-2022.)
Assertion
Ref Expression
19.41v (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v
StepHypRef Expression
1 19.40 1882 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1908 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 615 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 470 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1913 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 406 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 208 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775
This theorem is referenced by:  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  19.42v  1950  exdistrv  1952  r19.41v  3179  gencbvex  3527  euxfrw  3715  euxfr  3717  euind  3718  dfdif3  4113  zfpair  5425  opabn0  5559  eliunxp  5844  relop  5857  dmuni  5921  dminss  6164  imainss  6165  cnvresima  6241  rnco  6263  coass  6276  xpco  6300  rnoprab  7529  eloprabga  7533  f11o  7960  frxp  8140  omeu  8615  domen  8992  xpassen  9104  dif1enOLD  9200  enfii  9223  ttrclselem2  9769  kmlem3  10195  cflem  10289  genpass  11052  ltexprlem4  11082  hasheqf1oi  14368  elwspths2spth  29901  bnj534  34584  bnj906  34775  bnj908  34776  bnj916  34778  bnj983  34796  bnj986  34800  fmla0  35210  fmlasuc0  35212  rexxfr3dALT  35467  dftr6  35573  bj-eeanvw  36418  bj-substw  36427  bj-csbsnlem  36609  bj-clel3gALT  36755  bj-rest10  36795  bj-restuni  36804  bj-imdirco  36897  bj-ccinftydisj  36920  wl-dfclab  37291  eldmqsres2  37986  disjdmqscossss  38501  prter2  38579  dihglb2  41041  prjspeclsp  42266  pm11.6  44066  pm11.71  44071  rfcnnnub  44635  eliunxp2  47712  thinccic  48382
  Copyright terms: Public domain W3C validator