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 2044
Description: Version of 19.41 2268 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 2070. (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 1967 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 2007 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 610 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 463 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 2012 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 396 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 200 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875
This theorem is referenced by:  19.41vv  2045  19.41vvv  2046  19.41vvvv  2047  19.42v  2048  exdistrv  2050  equsexvw  2102  r19.41v  3236  gencbvex  3403  euxfr  3553  euind  3554  dfdif3  3884  zfpair  5062  opabn0  5169  eliunxp  5430  relop  5443  dmuni  5504  dminss  5732  imainss  5733  cnvresima  5811  rnco  5829  coass  5842  xpco  5863  rnoprab  6943  f11o  7328  frxp  7491  omeu  7872  domen  8175  xpassen  8263  kmlem3  9229  cflem  9323  genpass  10086  ltexprlem4  10116  hasheqf1oi  13347  elwspths2spth  27195  bnj534  31260  bnj906  31451  bnj908  31452  bnj916  31454  bnj983  31472  bnj986  31475  dftr6  32088  bj-eeanvw  33142  bj-cleljustab  33279  bj-csbsnlem  33326  bj-rest10  33472  bj-restuni  33481  bj-ccinftydisj  33537  wl-dv-sb  33758  eldmqsres2  34487  prter2  34840  dihglb2  37301  pm11.6  39269  pm11.71  39274  rfcnnnub  39850  eliunxp2  42784
  Copyright terms: Public domain W3C validator