Theorem r19.41v 3186

Description: Restricted quantifier version 19.41v 1951. Version of r19.41 3258 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 467	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1848	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1951	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 276	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 622	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1779   ∈ wcel 2104  ∃wrex 3068

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  r19.42v  3188  r19.41vv  3222  3reeanv  3225  reuxfr1d  3745  reuind  3748  iuncom4  5004  dfiun2gOLD  5033  iunxiun  5099  inuni  5342  xpiundi  5745  xpiundir  5746  imaco  6249  coiun  6254  abrexco  7245  imaiun  7246  isomin  7336  isoini  7337  imaeqsexv  7362  imaeqexov  7647  oarec  8564  mapsnend  9038  unfi  9174  brttrcl2  9711  genpass  11006  4fvwrd4  13625  4sqlem12  16893  imasleval  17491  lsmspsn  20839  utoptop  23959  metrest  24253  metust  24287  cfilucfil  24288  metuel2  24294  sleadd1  27711  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  addsdilem1  27845  istrkg2ld  27978  axsegcon  28452  fusgreg2wsp  29856  nmoo0  30311  nmop0  31506  nmfn0  31507  rexunirn  31999  dmrab  32004  iunrnmptss  32064  ressupprn  32179  ordtconnlem1  33202  dya2icoseg2  33575  dya2iocnei  33579  omssubaddlem  33596  omssubadd  33597  satfvsuclem2  34649  satf0  34661  satffunlem1lem2  34692  satffunlem2lem2  34695  bj-mpomptALT  36303  mptsnunlem  36522  fvineqsneq  36596  rabiun  36764  iundif1  36765  poimir  36824  ismblfin  36832  eldmqs1cossres  37832  erimeq2  37851  prter2  38054  prter3  38055  islshpat  38190  lshpsmreu  38282  islpln5  38709  islvol5  38753  cdlemftr3  39739  dvhb1dimN  40160  dib1dim  40339  mapdpglem3  40849  hdmapglem7a  41101  diophrex  41815  r19.41dv  47574