Theorem r19.41v 3191

Description: Restricted quantifier version 19.41v 1968. Version of r19.41 3265 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

Step	Hyp	Ref	Expression
1		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 472	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1867	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1968	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3086	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 226	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 636	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 301	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  r19.42v  3193  r19.41vv  3231  3reeanv  3234  reuxfr1d  3711  reuind  3714  iuncom4  4955  iunxiun  5051  inuni  5303  xpiundi  5714  xpiundir  5715  imaco  6233  coiun  6239  abrexco  7223  imaiun  7224  isomin  7316  isoini  7317  imaeqsexvOLD  7342  imaeqexov  7629  oarec  8525  mapsnend  9011  unfi  9133  brttrcl2  9663  genpass  10961  4fvwrd4  13647  4sqlem12  16983  imasleval  17562  lsmspsn  21139  utoptop  24282  metrest  24572  metust  24606  cfilucfil  24607  metuel2  24613  leadds1  28070  addsuniflem  28082  addsasslem1  28084  addsasslem2  28085  addsdilem1  28232  elreno2  28576  renegscl  28579  readdscl  28580  remulscl  28583  istrkg2ld  28617  axsegcon  29085  fusgreg2wsp  30495  nmoo0  30951  nmop0  32146  nmfn0  32147  rexunirn  32650  dmrab  32655  iunrnmptss  32725  ressupprn  32853  ordtconnlem1  34182  dya2icoseg2  34536  dya2iocnei  34540  omssubaddlem  34557  omssubadd  34558  r1omhf  35363  vonf1oonfo  35419  satfvsuclem2  35671  satf0  35683  satffunlem1lem2  35714  satffunlem2lem2  35717  rexxfr3dALT  35950  bj-mpomptALT  37570  mptsnunlem  37793  fvineqsneq  37867  rabiun  38053  iundif1  38054  poimir  38113  ismblfin  38121  eldmqs1cossres  39204  erimeq2  39223  prter2  39466  prter3  39467  islshpat  39602  lshpsmreu  39694  islpln5  40120  islvol5  40164  cdlemftr3  41150  dvhb1dimN  41571  dib1dim  41750  mapdpglem3  42260  hdmapglem7a  42512  diophrex  43317  dfsclnbgr6  48441  r19.41dv  49384  reuxfr1dd  49389