Theorem r19.41v 3273

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  r19.41vv  3275  r19.42v  3276  3reeanv  3293  reuxfr1d  3680  reuind  3683  iuncom4  4929  dfiun2g  4957  iunxiun  5022  inuni  5262  xpiundi  5648  xpiundir  5649  imaco  6144  coiun  6149  abrexco  7099  imaiun  7100  isomin  7188  isoini  7189  oarec  8355  mapsnend  8780  unfi  8917  genpass  10696  4fvwrd4  13305  4sqlem12  16585  imasleval  17169  lsmspsn  20261  utoptop  23294  metrest  23586  metust  23620  cfilucfil  23621  metuel2  23627  istrkg2ld  26725  axsegcon  27198  fusgreg2wsp  28601  nmoo0  29054  nmop0  30249  nmfn0  30250  rexunirn  30741  dmrab  30745  iunrnmptss  30806  ressupprn  30926  ordtconnlem1  31776  dya2icoseg2  32145  dya2iocnei  32149  omssubaddlem  32166  omssubadd  32167  satfvsuclem2  33222  satf0  33234  satffunlem1lem2  33265  satffunlem2lem2  33268  imaeqsexv  33593  brttrcl2  33700  bj-mpomptALT  35217  mptsnunlem  35436  fvineqsneq  35510  rabiun  35677  iundif1  35678  poimir  35737  ismblfin  35745  eldmqs1cossres  36698  erim2  36716  prter2  36822  prter3  36823  islshpat  36958  lshpsmreu  37050  islpln5  37476  islvol5  37520  cdlemftr3  38506  dvhb1dimN  38927  dib1dim  39106  mapdpglem3  39616  hdmapglem7a  39868  diophrex  40513  r19.41dv  46035