Theorem r19.41v 3189

Description: Restricted quantifier version 19.41v 1954. Version of r19.41 3261 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 470	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1851	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1954	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 277	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3072	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 625	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.42v  3191  r19.41vv  3225  3reeanv  3228  reuxfr1d  3747  reuind  3750  iuncom4  5006  dfiun2gOLD  5035  iunxiun  5101  inuni  5344  xpiundi  5747  xpiundir  5748  imaco  6251  coiun  6256  abrexco  7243  imaiun  7244  isomin  7334  isoini  7335  imaeqsexv  7360  imaeqexov  7645  oarec  8562  mapsnend  9036  unfi  9172  brttrcl2  9709  genpass  11004  4fvwrd4  13621  4sqlem12  16889  imasleval  17487  lsmspsn  20695  utoptop  23739  metrest  24033  metust  24067  cfilucfil  24068  metuel2  24074  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  addsdilem1  27606  istrkg2ld  27711  axsegcon  28185  fusgreg2wsp  29589  nmoo0  30044  nmop0  31239  nmfn0  31240  rexunirn  31732  dmrab  31737  iunrnmptss  31797  ressupprn  31912  ordtconnlem1  32904  dya2icoseg2  33277  dya2iocnei  33281  omssubaddlem  33298  omssubadd  33299  satfvsuclem2  34351  satf0  34363  satffunlem1lem2  34394  satffunlem2lem2  34397  bj-mpomptALT  36000  mptsnunlem  36219  fvineqsneq  36293  rabiun  36461  iundif1  36462  poimir  36521  ismblfin  36529  eldmqs1cossres  37529  erimeq2  37548  prter2  37751  prter3  37752  islshpat  37887  lshpsmreu  37979  islpln5  38406  islvol5  38450  cdlemftr3  39436  dvhb1dimN  39857  dib1dim  40036  mapdpglem3  40546  hdmapglem7a  40798  diophrex  41513  r19.41dv  47487