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 3081
Description: Restricted quantifier version 19.41v 1911. Version of r19.41 3082 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 680 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1771 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1911 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 266 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 2913 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 2913 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 730 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-rex 2913
This theorem is referenced by:  r19.41vv  3083  r19.42v  3084  3reeanv  3098  reuind  3393  iuncom4  4494  dfiun2g  4518  iunxiun  4574  inuni  4786  reuxfrd  4853  xpiundi  5134  xpiundir  5135  imaco  5599  coiun  5604  abrexco  6456  imaiun  6457  isomin  6541  isoini  6542  oarec  7587  mapsnen  7979  genpass  9775  4fvwrd4  12400  4sqlem12  15584  imasleval  16122  lsmspsn  19003  utoptop  21948  metrest  22239  metust  22273  cfilucfil  22274  metuel2  22280  istrkg2ld  25259  axsegcon  25707  fusgreg2wsp  27058  nmoo0  27492  hhcmpl  27903  nmop0  28691  nmfn0  28692  reuxfr4d  29176  rexunirn  29177  ordtconnlem1  29749  dya2icoseg2  30118  dya2iocnei  30122  omssubaddlem  30139  omssubadd  30140  bj-mpt2mptALT  32706  mptsnunlem  32814  rabiun  33011  iundif1  33012  poimir  33071  ismblfin  33079  prtlem11  33628  prter2  33643  prter3  33644  islshpat  33781  lshpsmreu  33873  islpln5  34298  islvol5  34342  cdlemftr3  35330  dvhb1dimN  35751  dib1dim  35931  mapdpglem3  36441  hdmapglem7a  36696  diophrex  36816  mapsnend  38862
  Copyright terms: Public domain W3C validator