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 3118
Description: Restricted quantifier version 19.41v 1917. Version of r19.41 3119 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 682 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1814 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1917 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 266 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 2947 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 2947 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 731 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1744  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  r19.41vv  3120  r19.42v  3121  3reeanv  3137  reuind  3444  iuncom4  4560  dfiun2g  4584  iunxiun  4640  inuni  4856  reuxfrd  4923  xpiundi  5207  xpiundir  5208  imaco  5678  coiun  5683  abrexco  6542  imaiun  6543  isomin  6627  isoini  6628  oarec  7687  mapsnen  8076  genpass  9869  4fvwrd4  12498  4sqlem12  15707  imasleval  16248  lsmspsn  19132  utoptop  22085  metrest  22376  metust  22410  cfilucfil  22411  metuel2  22417  istrkg2ld  25404  axsegcon  25852  fusgreg2wsp  27316  nmoo0  27774  hhcmpl  28185  nmop0  28973  nmfn0  28974  reuxfr4d  29457  rexunirn  29458  ordtconnlem1  30098  dya2icoseg2  30468  dya2iocnei  30472  omssubaddlem  30489  omssubadd  30490  bj-mpt2mptALT  33197  mptsnunlem  33315  rabiun  33512  iundif1  33513  poimir  33572  ismblfin  33580  prtlem11  34470  prter2  34485  prter3  34486  islshpat  34622  lshpsmreu  34714  islpln5  35139  islvol5  35183  cdlemftr3  36170  dvhb1dimN  36591  dib1dim  36771  mapdpglem3  37281  hdmapglem7a  37536  diophrex  37656  mapsnend  39705
  Copyright terms: Public domain W3C validator