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 3178
Description: Restricted quantifier version 19.41v 1945. Version of r19.41 3250 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 df-rex 3060 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
2 anass 467 . . 3 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
32exbii 1842 . 2 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
4 19.41v 1945 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3060 . . . 4 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
65bicomi 223 . . 3 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥𝐴 𝜑)
74, 6bianbi 625 . 2 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
81, 3, 73bitr2i 298 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wex 1773  wcel 2098  wrex 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060
This theorem is referenced by:  r19.42v  3180  r19.41vv  3214  3reeanv  3217  reuxfr1d  3742  reuind  3745  iuncom4  5005  dfiun2gOLD  5035  iunxiun  5101  inuni  5346  xpiundi  5748  xpiundir  5749  imaco  6257  coiun  6262  abrexco  7254  imaiun  7255  isomin  7344  isoini  7345  imaeqsexv  7370  imaeqexov  7659  oarec  8583  mapsnend  9061  unfi  9197  brttrcl2  9739  genpass  11034  4fvwrd4  13656  4sqlem12  16928  imasleval  17526  lsmspsn  20981  utoptop  24183  metrest  24477  metust  24511  cfilucfil  24512  metuel2  24518  sleadd1  27952  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  addsdilem1  28101  0reno  28297  renegscl  28298  readdscl  28299  remulscl  28302  istrkg2ld  28336  axsegcon  28810  fusgreg2wsp  30218  nmoo0  30673  nmop0  31868  nmfn0  31869  rexunirn  32368  dmrab  32373  iunrnmptss  32435  ressupprn  32552  ordtconnlem1  33656  dya2icoseg2  34029  dya2iocnei  34033  omssubaddlem  34050  omssubadd  34051  satfvsuclem2  35101  satf0  35113  satffunlem1lem2  35144  satffunlem2lem2  35147  bj-mpomptALT  36729  mptsnunlem  36948  fvineqsneq  37022  rabiun  37197  iundif1  37198  poimir  37257  ismblfin  37265  eldmqs1cossres  38261  erimeq2  38280  prter2  38483  prter3  38484  islshpat  38619  lshpsmreu  38711  islpln5  39138  islvol5  39182  cdlemftr3  40168  dvhb1dimN  40589  dib1dim  40768  mapdpglem3  41278  hdmapglem7a  41530  diophrex  42337  dfsclnbgr6  47330  r19.41dv  48060
  Copyright terms: Public domain W3C validator