MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.41v Structured version   Visualization version   GIF version

Theorem r19.41v 3182
Description: Restricted quantifier version 19.41v 1954. Version of r19.41 3245 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
Assertion
Ref Expression
r19.41v (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.41v
StepHypRef Expression
1 anass 470 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1851 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1954 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 277 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3071 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 3071 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 625 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 303 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  wrex 3070
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  df-rex 3071
This theorem is referenced by:  r19.42v  3184  r19.41vv  3214  3reeanv  3217  reuxfr1d  3709  reuind  3712  iuncom4  4963  dfiun2gOLD  4992  iunxiun  5058  inuni  5301  xpiundi  5703  xpiundir  5704  imaco  6204  coiun  6209  abrexco  7192  imaiun  7193  isomin  7283  isoini  7284  imaeqsexv  7309  imaeqexov  7593  oarec  8510  mapsnend  8983  unfi  9119  brttrcl2  9655  genpass  10950  4fvwrd4  13567  4sqlem12  16833  imasleval  17428  lsmspsn  20560  utoptop  23602  metrest  23896  metust  23930  cfilucfil  23931  metuel2  23937  sleadd1  27320  addsunif  27332  addsasslem1  27333  addsasslem2  27334  istrkg2ld  27444  axsegcon  27918  fusgreg2wsp  29322  nmoo0  29775  nmop0  30970  nmfn0  30971  rexunirn  31463  dmrab  31468  iunrnmptss  31530  ressupprn  31651  ordtconnlem1  32562  dya2icoseg2  32935  dya2iocnei  32939  omssubaddlem  32956  omssubadd  32957  satfvsuclem2  34011  satf0  34023  satffunlem1lem2  34054  satffunlem2lem2  34057  bj-mpomptALT  35636  mptsnunlem  35855  fvineqsneq  35929  rabiun  36097  iundif1  36098  poimir  36157  ismblfin  36165  eldmqs1cossres  37167  erimeq2  37186  prter2  37389  prter3  37390  islshpat  37525  lshpsmreu  37617  islpln5  38044  islvol5  38088  cdlemftr3  39074  dvhb1dimN  39495  dib1dim  39674  mapdpglem3  40184  hdmapglem7a  40436  diophrex  41141  r19.41dv  46973
  Copyright terms: Public domain W3C validator