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

Theorem r19.41v 3328
 Description: Restricted quantifier version 19.41v 1950. Version of r19.41 3329 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 472 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1849 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1950 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 280 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3136 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 3136 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 626 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 306 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2114  ∃wrex 3131 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  df-rex 3136 This theorem is referenced by:  r19.41vv  3330  r19.42v  3331  3reeanv  3349  reuxfr1d  3716  reuind  3719  iuncom4  4902  dfiun2g  4930  dfiun2gOLD  4931  iunxiun  4994  inuni  5222  xpiundi  5599  xpiundir  5600  imaco  6082  coiun  6087  abrexco  6986  imaiun  6987  isomin  7074  isoini  7075  oarec  8175  mapsnend  8575  genpass  10420  4fvwrd4  13022  4sqlem12  16281  imasleval  16805  lsmspsn  19847  utoptop  22838  metrest  23129  metust  23163  cfilucfil  23164  metuel2  23170  istrkg2ld  26252  axsegcon  26719  fusgreg2wsp  28119  nmoo0  28572  nmop0  29767  nmfn0  29768  rexunirn  30261  dmrab  30265  iunrnmptss  30324  ordtconnlem1  31241  dya2icoseg2  31610  dya2iocnei  31614  omssubaddlem  31631  omssubadd  31632  satfvsuclem2  32681  satf0  32693  satffunlem1lem2  32724  satffunlem2lem2  32727  bj-mpomptALT  34495  mptsnunlem  34716  fvineqsneq  34790  rabiun  34988  iundif1  34989  poimir  35048  ismblfin  35056  eldmqs1cossres  36011  erim2  36029  prter2  36135  prter3  36136  islshpat  36271  lshpsmreu  36363  islpln5  36789  islvol5  36833  cdlemftr3  37819  dvhb1dimN  38240  dib1dim  38419  mapdpglem3  38929  hdmapglem7a  39181  diophrex  39646
 Copyright terms: Public domain W3C validator