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

Theorem r19.41v 3070
 Description: Restricted quantifier version 19.41v 1901. Version of r19.41 3071 with a dv 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 679 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1764 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1901 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 265 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 2902 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 2902 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 727 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 291 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902 This theorem is referenced by:  r19.41vv  3072  r19.42v  3073  3reeanv  3087  reuind  3378  iuncom4  4464  dfiun2g  4488  iunxiun  4544  inuni  4753  reuxfrd  4819  xpiundi  5096  xpiundir  5097  imaco  5557  coiun  5562  abrexco  6406  imaiun  6407  isomin  6487  isoini  6488  oarec  7529  mapsnen  7920  genpass  9710  4fvwrd4  12328  4sqlem12  15498  imasleval  16024  lsmspsn  18905  utoptop  21848  metrest  22139  metust  22173  cfilucfil  22174  metuel2  22180  istrkg2ld  25159  axsegcon  25607  usgreg2spot  26594  nmoo0  27030  hhcmpl  27441  nmop0  28229  nmfn0  28230  reuxfr4d  28714  rexunirn  28715  ordtconlem1  29298  dya2icoseg2  29667  dya2iocnei  29671  omssubaddlem  29688  omssubadd  29689  nofulllem5  31105  bj-mpt2mptALT  32253  mptsnunlem  32361  rabiun  32552  iundif1  32553  poimir  32612  ismblfin  32620  prtlem11  33169  prter2  33184  prter3  33185  islshpat  33322  lshpsmreu  33414  islpln5  33839  islvol5  33883  cdlemftr3  34871  dvhb1dimN  35292  dib1dim  35472  mapdpglem3  35982  hdmapglem7a  36237  diophrex  36357  mapsnend  38386  fusgreg2wsp  41500
 Copyright terms: Public domain W3C validator