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 1950
Description: Version of 19.41 2236 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1970. (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 1887 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1913 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 619 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 475 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1918 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 411 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 212 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782
This theorem is referenced by:  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  19.42v  1954  exdistrv  1956  equsexvwOLD  2012  r19.41v  3303  gencbvex  3500  euxfrw  3663  euxfr  3665  euind  3666  dfdif3  4045  zfpair  5290  opabn0  5408  eliunxp  5676  relop  5689  dmuni  5751  dminss  5981  imainss  5982  cnvresima  6058  rnco  6076  coass  6089  xpco  6112  rnoprab  7240  f11o  7634  frxp  7807  omeu  8198  domen  8509  xpassen  8598  kmlem3  9567  cflem  9661  genpass  10424  ltexprlem4  10454  hasheqf1oi  13712  elwspths2spth  27756  bnj534  32118  bnj906  32310  bnj908  32311  bnj916  32313  bnj983  32331  bnj986  32335  fmla0  32737  fmlasuc0  32739  dftr6  33094  bj-eeanvw  34155  bj-substw  34164  bj-csbsnlem  34339  bj-rest10  34498  bj-restuni  34507  bj-imdirco  34600  bj-ccinftydisj  34623  wl-dfclab  34986  eldmqsres2  35697  prter2  36170  dihglb2  38631  prjspeclsp  39593  pm11.6  41083  pm11.71  41088  rfcnnnub  41652  eliunxp2  44722
  Copyright terms: Public domain W3C validator