Theorem r19.41v 3167

Description: Restricted quantifier version 19.41v 1951. Version of r19.41 3241 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 3062	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1850	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1951	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3062	. . . 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 3061

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 3062

This theorem is referenced by:  r19.42v  3169  r19.41vv  3207  3reeanv  3210  reuxfr1d  3696  reuind  3699  iuncom4  4942  iunxiun  5039  inuni  5291  xpiundi  5702  xpiundir  5703  imaco  6215  coiun  6221  abrexco  7199  imaiun  7200  isomin  7292  isoini  7293  imaeqsexvOLD  7318  imaeqexov  7605  oarec  8497  mapsnend  8983  unfi  9105  brttrcl2  9635  genpass  10932  4fvwrd4  13602  4sqlem12  16927  imasleval  17505  lsmspsn  21079  utoptop  24199  metrest  24489  metust  24523  cfilucfil  24524  metuel2  24530  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  addsdilem1  28143  elreno2  28487  renegscl  28490  readdscl  28491  remulscl  28494  istrkg2ld  28528  axsegcon  28996  fusgreg2wsp  30406  nmoo0  30862  nmop0  32057  nmfn0  32058  rexunirn  32561  dmrab  32566  iunrnmptss  32635  ressupprn  32763  ordtconnlem1  34068  dya2icoseg2  34422  dya2iocnei  34426  omssubaddlem  34443  omssubadd  34444  r1omhf  35249  satfvsuclem2  35542  satf0  35554  satffunlem1lem2  35585  satffunlem2lem2  35588  rexxfr3dALT  35821  bj-mpomptALT  37431  mptsnunlem  37654  fvineqsneq  37728  rabiun  37914  iundif1  37915  poimir  37974  ismblfin  37982  eldmqs1cossres  39065  erimeq2  39084  prter2  39327  prter3  39328  islshpat  39463  lshpsmreu  39555  islpln5  39981  islvol5  40025  cdlemftr3  41011  dvhb1dimN  41432  dib1dim  41611  mapdpglem3  42121  hdmapglem7a  42373  diophrex  43207  dfsclnbgr6  48334  r19.41dv  49277  reuxfr1dd  49282