Theorem r19.41v 3070

Description: Restricted quantifier version 19.41v 1901. Version of r19.41 3071 with a dv 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 679	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1764	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1901	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 265	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 2902	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 2902	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 727	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 291	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902

This theorem is referenced by:  r19.41vv  3072  r19.42v  3073  3reeanv  3087  reuind  3378  iuncom4  4464  dfiun2g  4488  iunxiun  4544  inuni  4753  reuxfrd  4819  xpiundi  5096  xpiundir  5097  imaco  5557  coiun  5562  abrexco  6406  imaiun  6407  isomin  6487  isoini  6488  oarec  7529  mapsnen  7920  genpass  9710  4fvwrd4  12328  4sqlem12  15498  imasleval  16024  lsmspsn  18905  utoptop  21848  metrest  22139  metust  22173  cfilucfil  22174  metuel2  22180  istrkg2ld  25159  axsegcon  25607  usgreg2spot  26594  nmoo0  27030  hhcmpl  27441  nmop0  28229  nmfn0  28230  reuxfr4d  28714  rexunirn  28715  ordtconlem1  29298  dya2icoseg2  29667  dya2iocnei  29671  omssubaddlem  29688  omssubadd  29689  nofulllem5  31105  bj-mpt2mptALT  32253  mptsnunlem  32361  rabiun  32552  iundif1  32553  poimir  32612  ismblfin  32620  prtlem11  33169  prter2  33184  prter3  33185  islshpat  33322  lshpsmreu  33414  islpln5  33839  islvol5  33883  cdlemftr3  34871  dvhb1dimN  35292  dib1dim  35472  mapdpglem3  35982  hdmapglem7a  36237  diophrex  36357  mapsnend  38386  fusgreg2wsp  41500