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 1927
Description: Version of 19.41 2202 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1947. (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 1868 . . 3 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2 ax5e 1890 . . . 4 (∃𝑥𝜓𝜓)
32anim2i 616 . . 3 ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑𝜓))
41, 3syl 17 . 2 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑𝜓))
5 pm3.21 472 . . . 4 (𝜓 → (𝜑 → (𝜑𝜓)))
65eximdv 1895 . . 3 (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))
76impcom 408 . 2 ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓))
84, 7impbii 210 1 (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wex 1761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762
This theorem is referenced by:  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  19.42v  1931  exdistrv  1933  equsexvwOLD  1989  r19.41v  3308  gencbvex  3492  euxfr  3648  euind  3649  dfdif3  4012  zfpair  5213  opabn0  5328  eliunxp  5594  relop  5607  dmuni  5669  dminss  5886  imainss  5887  cnvresima  5962  rnco  5980  coass  5993  xpco  6015  rnoprab  7113  f11o  7504  frxp  7673  omeu  8061  domen  8370  xpassen  8458  kmlem3  9424  cflem  9514  genpass  10277  ltexprlem4  10307  hasheqf1oi  13562  elwspths2spth  27433  bnj534  31627  bnj906  31818  bnj908  31819  bnj916  31821  bnj983  31839  bnj986  31842  fmla0  32237  fmlasuc0  32239  dftr6  32594  bj-eeanvw  33646  bj-csbsnlem  33791  bj-rest10  33978  bj-restuni  33987  bj-ccinftydisj  34053  wl-dfclab  34359  eldmqsres2  35076  prter2  35548  dihglb2  38009  prjspeclsp  38759  pm11.6  40262  pm11.71  40267  rfcnnnub  40832  eliunxp2  43860
  Copyright terms: Public domain W3C validator