Theorem r19.41v 3300

Description: Restricted quantifier version 19.41v 1950. Version of r19.41 3301 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		anass 472	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1849	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1950	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 280	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3112	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3112	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 626	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  r19.41vv  3302  r19.42v  3303  3reeanv  3321  reuxfr1d  3689  reuind  3692  iuncom4  4889  dfiun2g  4917  dfiun2gOLD  4918  iunxiun  4982  inuni  5210  xpiundi  5586  xpiundir  5587  imaco  6071  coiun  6076  abrexco  6981  imaiun  6982  isomin  7069  isoini  7070  oarec  8171  mapsnend  8571  genpass  10420  4fvwrd4  13022  4sqlem12  16282  imasleval  16806  lsmspsn  19849  utoptop  22840  metrest  23131  metust  23165  cfilucfil  23166  metuel2  23172  istrkg2ld  26254  axsegcon  26721  fusgreg2wsp  28121  nmoo0  28574  nmop0  29769  nmfn0  29770  rexunirn  30263  dmrab  30267  iunrnmptss  30329  ressupprn  30450  ordtconnlem1  31277  dya2icoseg2  31646  dya2iocnei  31650  omssubaddlem  31667  omssubadd  31668  satfvsuclem2  32720  satf0  32732  satffunlem1lem2  32763  satffunlem2lem2  32766  bj-mpomptALT  34534  mptsnunlem  34755  fvineqsneq  34829  rabiun  35030  iundif1  35031  poimir  35090  ismblfin  35098  eldmqs1cossres  36053  erim2  36071  prter2  36177  prter3  36178  islshpat  36313  lshpsmreu  36405  islpln5  36831  islvol5  36875  cdlemftr3  37861  dvhb1dimN  38282  dib1dim  38461  mapdpglem3  38971  hdmapglem7a  39223  diophrex  39716