Theorem r19.41v 3347

Description: Restricted quantifier version 19.41v 1950. Version of r19.41 3348 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 471	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1848	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1950	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 279	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3144	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3144	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 625	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  r19.41vv  3349  r19.42v  3350  3reeanv  3368  reuxfr1d  3741  reuind  3744  iuncom4  4927  dfiun2g  4955  dfiun2gOLD  4956  iunxiun  5019  inuni  5246  xpiundi  5622  xpiundir  5623  imaco  6104  coiun  6109  abrexco  7003  imaiun  7004  isomin  7090  isoini  7091  oarec  8188  mapsnend  8588  genpass  10431  4fvwrd4  13028  4sqlem12  16292  imasleval  16814  lsmspsn  19856  utoptop  22843  metrest  23134  metust  23168  cfilucfil  23169  metuel2  23175  istrkg2ld  26246  axsegcon  26713  fusgreg2wsp  28115  nmoo0  28568  nmop0  29763  nmfn0  29764  rexunirn  30256  dmrab  30260  iunrnmptss  30317  ordtconnlem1  31167  dya2icoseg2  31536  dya2iocnei  31540  omssubaddlem  31557  omssubadd  31558  satfvsuclem2  32607  satf0  32619  satffunlem1lem2  32650  satffunlem2lem2  32653  bj-mpomptALT  34414  mptsnunlem  34622  fvineqsneq  34696  rabiun  34880  iundif1  34881  poimir  34940  ismblfin  34948  eldmqs1cossres  35908  erim2  35926  prter2  36032  prter3  36033  islshpat  36168  lshpsmreu  36260  islpln5  36686  islvol5  36730  cdlemftr3  37716  dvhb1dimN  38137  dib1dim  38316  mapdpglem3  38826  hdmapglem7a  39078  diophrex  39392