Theorem r19.41v 3168

Description: Restricted quantifier version 19.41v 1951. Version of r19.41 3242 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 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1850	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1951	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3063	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 628	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.42v  3170  r19.41vv  3208  3reeanv  3211  reuxfr1d  3710  reuind  3713  iuncom4  4957  iunxiun  5054  inuni  5297  xpiundi  5703  xpiundir  5704  imaco  6217  coiun  6223  abrexco  7200  imaiun  7201  isomin  7293  isoini  7294  imaeqsexvOLD  7319  imaeqexov  7606  oarec  8499  mapsnend  8985  unfi  9107  brttrcl2  9635  genpass  10932  4fvwrd4  13576  4sqlem12  16896  imasleval  17474  lsmspsn  21048  utoptop  24190  metrest  24480  metust  24514  cfilucfil  24515  metuel2  24521  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  addsdilem1  28159  elreno2  28503  renegscl  28506  readdscl  28507  remulscl  28510  istrkg2ld  28544  axsegcon  29012  fusgreg2wsp  30423  nmoo0  30879  nmop0  32074  nmfn0  32075  rexunirn  32578  dmrab  32583  iunrnmptss  32652  ressupprn  32780  ordtconnlem1  34102  dya2icoseg2  34456  dya2iocnei  34460  omssubaddlem  34477  omssubadd  34478  r1omhf  35283  satfvsuclem2  35576  satf0  35588  satffunlem1lem2  35619  satffunlem2lem2  35622  rexxfr3dALT  35855  bj-mpomptALT  37372  mptsnunlem  37593  fvineqsneq  37667  rabiun  37844  iundif1  37845  poimir  37904  ismblfin  37912  eldmqs1cossres  38995  erimeq2  39014  prter2  39257  prter3  39258  islshpat  39393  lshpsmreu  39485  islpln5  39911  islvol5  39955  cdlemftr3  40941  dvhb1dimN  41362  dib1dim  41541  mapdpglem3  42051  hdmapglem7a  42303  diophrex  43132  dfsclnbgr6  48218  r19.41dv  49161  reuxfr1dd  49166