Theorem r19.41v 3195

Description: Restricted quantifier version 19.41v 1979. Version of r19.41 3269 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		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 473	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1878	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1979	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3090	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 227	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 638	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  r19.42v  3197  r19.41vv  3235  3reeanv  3238  reuxfr1d  3714  reuind  3717  iuncom4  4966  iunxiun  5064  inuni  5322  xpiundi  5734  xpiundir  5735  imaco  6254  coiun  6260  abrexco  7244  imaiun  7245  isomin  7337  isoini  7338  imaeqsexvOLD  7363  imaeqexov  7650  oarec  8548  mapsnend  9034  unfi  9156  brttrcl2  9684  genpass  10995  4fvwrd4  13678  4sqlem12  17017  imasleval  17596  lsmspsn  21186  utoptop  24372  metrest  24662  metust  24696  cfilucfil  24697  metuel2  24703  leadds1  28163  addsuniflem  28175  addsasslem1  28177  addsasslem2  28178  addsdilem1  28325  elreno2  28669  renegscl  28672  readdscl  28673  remulscl  28676  istrkg2ld  28710  axsegcon  29258  fusgreg2wsp  30668  nmoo0  31124  nmop0  32319  nmfn0  32320  rexunirn  32819  dmrab  32824  iunrnmptss  32891  ressupprn  33016  ordtconnlem1  34295  dya2icoseg2  34649  dya2iocnei  34653  omssubaddlem  34670  omssubadd  34671  r1omhf  35481  vonf1oonfo  35580  satfvsuclem2  35833  satf0  35845  satffunlem1lem2  35876  satffunlem2lem2  35879  rexxfr3dALT  36112  bj-mpomptALT  37742  mptsnunlem  37965  fvineqsneq  38039  rabiun  38225  iundif1  38226  poimir  38285  ismblfin  38293  eldmqs1cossres  39374  erimeq2  39393  prter2  39636  prter3  39637  islshpat  39772  lshpsmreu  39864  islpln5  40290  islvol5  40334  cdlemftr3  41320  dvhb1dimN  41741  dib1dim  41920  mapdpglem3  42430  hdmapglem7a  42682  diophrex  43489  dfsclnbgr6  48606  r19.41dv  49563  reuxfr1dd  49568