Theorem r19.41v 3282

Description: Restricted quantifier version 19.41v 1908. Version of r19.41 3283 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 461	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1810	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1908	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 269	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3088	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 614	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 295	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 387  ∃wex 1742   ∈ wcel 2048  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088

This theorem is referenced by:  r19.41vv  3284  r19.42v  3285  3reeanv  3303  reuxfr4d  3648  reuind  3649  iuncom4  4794  dfiun2g  4819  dfiun2gOLD  4820  iunxiun  4879  inuni  5096  reuxfrd  5168  xpiundi  5465  xpiundir  5466  imaco  5937  coiun  5942  abrexco  6822  imaiun  6823  isomin  6907  isoini  6908  oarec  7981  mapsnend  8377  genpass  10221  4fvwrd4  12836  4sqlem12  16138  imasleval  16660  lsmspsn  19568  utoptop  22536  metrest  22827  metust  22861  cfilucfil  22862  metuel2  22868  istrkg2ld  25938  axsegcon  26406  fusgreg2wsp  27860  nmoo0  28335  nmop0  29534  nmfn0  29535  rexunirn  30027  dmrab  30029  iunrnmptss  30076  ordtconnlem1  30768  dya2icoseg2  31138  dya2iocnei  31142  omssubaddlem  31159  omssubadd  31160  bj-mpt2mptALT  33855  mptsnunlem  33996  fvineqsneq  34069  rabiun  34254  iundif1  34255  poimir  34314  ismblfin  34322  eldmqs1cossres  35286  erim2  35304  prter2  35410  prter3  35411  islshpat  35546  lshpsmreu  35638  islpln5  36064  islvol5  36108  cdlemftr3  37094  dvhb1dimN  37515  dib1dim  37694  mapdpglem3  38204  hdmapglem7a  38456  diophrex  38713