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 3282
Description: Restricted quantifier version 19.41v 1908. Version of r19.41 3283 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 461 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1810 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1908 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 269 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3088 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 3088 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 614 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 295 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 387  wex 1742  wcel 2048  wrex 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088
This theorem is referenced by:  r19.41vv  3284  r19.42v  3285  3reeanv  3303  reuxfr4d  3648  reuind  3649  iuncom4  4794  dfiun2g  4819  dfiun2gOLD  4820  iunxiun  4879  inuni  5096  reuxfrd  5168  xpiundi  5465  xpiundir  5466  imaco  5937  coiun  5942  abrexco  6822  imaiun  6823  isomin  6907  isoini  6908  oarec  7981  mapsnend  8377  genpass  10221  4fvwrd4  12836  4sqlem12  16138  imasleval  16660  lsmspsn  19568  utoptop  22536  metrest  22827  metust  22861  cfilucfil  22862  metuel2  22868  istrkg2ld  25938  axsegcon  26406  fusgreg2wsp  27860  nmoo0  28335  nmop0  29534  nmfn0  29535  rexunirn  30027  dmrab  30029  iunrnmptss  30076  ordtconnlem1  30768  dya2icoseg2  31138  dya2iocnei  31142  omssubaddlem  31159  omssubadd  31160  bj-mpt2mptALT  33855  mptsnunlem  33996  fvineqsneq  34069  rabiun  34254  iundif1  34255  poimir  34314  ismblfin  34322  eldmqs1cossres  35286  erim2  35304  prter2  35410  prter3  35411  islshpat  35546  lshpsmreu  35638  islpln5  36064  islvol5  36108  cdlemftr3  37094  dvhb1dimN  37515  dib1dim  37694  mapdpglem3  38204  hdmapglem7a  38456  diophrex  38713
  Copyright terms: Public domain W3C validator