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 1949
Description: Version of 19.41 2235 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1967. (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 1886 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1912 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 617 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 471 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1917 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 407 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 209 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  19.42v  1953  exdistrv  1955  r19.41v  3189  gencbvex  3541  euxfrw  3727  euxfr  3729  euind  3730  dfdif3OLD  4118  zfpair  5421  opabn0  5558  eliunxp  5848  relop  5861  dmuni  5925  dminss  6173  imainss  6174  cnvresima  6250  rnco  6272  coass  6285  xpco  6309  rnoprab  7538  eloprabga  7542  f11o  7971  frxp  8151  omeu  8623  domen  9002  xpassen  9106  dif1enOLD  9202  enfii  9226  ttrclselem2  9766  kmlem3  10193  cflem  10285  cflemOLD  10286  genpass  11049  ltexprlem4  11079  hasheqf1oi  14390  elwspths2spth  29987  bnj534  34753  bnj906  34944  bnj908  34945  bnj916  34947  bnj983  34965  bnj986  34969  fmla0  35387  fmlasuc0  35389  rexxfr3dALT  35644  dftr6  35751  bj-eeanvw  36714  bj-substw  36723  bj-csbsnlem  36904  bj-clel3gALT  37049  bj-rest10  37089  bj-restuni  37098  bj-imdirco  37191  bj-ccinftydisj  37214  wl-dfclab  37597  eldmqsres2  38289  disjdmqscossss  38804  prter2  38882  dihglb2  41344  prjspeclsp  42622  pm11.6  44411  pm11.71  44416  rfcnnnub  45041  eliunxp2  48250  thinccic  49118
  Copyright terms: Public domain W3C validator