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 1954
Description: Version of 19.41 2229 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1972. (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 1890 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1916 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 618 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 473 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1921 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 409 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 208 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  19.42v  1958  exdistrv  1960  r19.41v  3186  gencbvex  3507  euxfrw  3684  euxfr  3686  euind  3687  dfdif3  4079  zfpair  5381  opabn0  5515  eliunxp  5798  relop  5811  dmuni  5875  dminss  6110  imainss  6111  cnvresima  6187  rnco  6209  coass  6222  xpco  6246  rnoprab  7465  eloprabga  7469  f11o  7884  frxp  8063  omeu  8537  domen  8908  xpassen  9017  dif1enOLD  9113  enfii  9140  ttrclselem2  9669  kmlem3  10095  cflem  10189  genpass  10952  ltexprlem4  10982  hasheqf1oi  14258  elwspths2spth  28954  bnj534  33391  bnj906  33582  bnj908  33583  bnj916  33585  bnj983  33603  bnj986  33607  fmla0  34016  fmlasuc0  34018  dftr6  34363  bj-eeanvw  35207  bj-substw  35216  bj-csbsnlem  35399  bj-clel3gALT  35548  bj-rest10  35588  bj-restuni  35597  bj-imdirco  35690  bj-ccinftydisj  35713  wl-dfclab  36077  eldmqsres2  36777  disjdmqscossss  37294  prter2  37372  dihglb2  39834  prjspeclsp  40979  pm11.6  42746  pm11.71  42751  rfcnnnub  43315  eliunxp2  46483  thinccic  47155
  Copyright terms: Public domain W3C validator