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 3189
Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3263 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 3071 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
2 anass 468 . . 3 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
32exbii 1848 . 2 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
4 19.41v 1949 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3071 . . . 4 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
65bicomi 224 . . 3 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥𝐴 𝜑)
74, 6bianbi 627 . 2 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
81, 3, 73bitr2i 299 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779  wcel 2108  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071
This theorem is referenced by:  r19.42v  3191  r19.41vv  3227  3reeanv  3230  reuxfr1d  3756  reuind  3759  iuncom4  5000  dfiun2gOLD  5031  iunxiun  5097  inuni  5350  xpiundi  5756  xpiundir  5757  imaco  6271  coiun  6276  abrexco  7264  imaiun  7265  isomin  7357  isoini  7358  imaeqsexvOLD  7383  imaeqexov  7671  oarec  8600  mapsnend  9076  unfi  9211  brttrcl2  9754  genpass  11049  4fvwrd4  13688  4sqlem12  16994  imasleval  17586  lsmspsn  21083  utoptop  24243  metrest  24537  metust  24571  cfilucfil  24572  metuel2  24578  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  addsdilem1  28177  0reno  28429  renegscl  28430  readdscl  28431  remulscl  28434  istrkg2ld  28468  axsegcon  28942  fusgreg2wsp  30355  nmoo0  30810  nmop0  32005  nmfn0  32006  rexunirn  32511  dmrab  32516  iunrnmptss  32578  ressupprn  32699  ordtconnlem1  33923  dya2icoseg2  34280  dya2iocnei  34284  omssubaddlem  34301  omssubadd  34302  satfvsuclem2  35365  satf0  35377  satffunlem1lem2  35408  satffunlem2lem2  35411  rexxfr3dALT  35644  bj-mpomptALT  37120  mptsnunlem  37339  fvineqsneq  37413  rabiun  37600  iundif1  37601  poimir  37660  ismblfin  37668  eldmqs1cossres  38660  erimeq2  38679  prter2  38882  prter3  38883  islshpat  39018  lshpsmreu  39110  islpln5  39537  islvol5  39581  cdlemftr3  40567  dvhb1dimN  40988  dib1dim  41167  mapdpglem3  41677  hdmapglem7a  41929  diophrex  42786  dfsclnbgr6  47844  r19.41dv  48722  reuxfr1dd  48726
  Copyright terms: Public domain W3C validator