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 3219
Description: Restricted quantifier version 19.41v 2018. Version of r19.41 3220 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 684 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1915 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 2018 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 266 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3048 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 3048 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 733 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1845  wcel 2131  wrex 3043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-rex 3048
This theorem is referenced by:  r19.41vv  3221  r19.42v  3222  3reeanv  3238  reuind  3544  iuncom4  4672  dfiun2g  4696  iunxiun  4752  inuni  4967  reuxfrd  5034  xpiundi  5322  xpiundir  5323  imaco  5793  coiun  5798  abrexco  6657  imaiun  6658  isomin  6742  isoini  6743  oarec  7803  mapsnen  8192  genpass  10015  4fvwrd4  12645  4sqlem12  15854  imasleval  16395  lsmspsn  19278  utoptop  22231  metrest  22522  metust  22556  cfilucfil  22557  metuel2  22563  istrkg2ld  25550  axsegcon  25998  fusgreg2wsp  27482  nmoo0  27947  hhcmpl  28358  nmop0  29146  nmfn0  29147  reuxfr4d  29630  rexunirn  29631  ordtconnlem1  30271  dya2icoseg2  30641  dya2iocnei  30645  omssubaddlem  30662  omssubadd  30663  bj-mpt2mptALT  33370  mptsnunlem  33488  rabiun  33687  iundif1  33688  poimir  33747  ismblfin  33755  prtlem11  34647  prter2  34662  prter3  34663  islshpat  34799  lshpsmreu  34891  islpln5  35316  islvol5  35360  cdlemftr3  36347  dvhb1dimN  36768  dib1dim  36948  mapdpglem3  37458  hdmapglem7a  37713  diophrex  37833  mapsnend  39882
  Copyright terms: Public domain W3C validator