Theorem r19.41v 3174

Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3246 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 3061	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1848	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1949	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3061	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 627	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  r19.42v  3176  r19.41vv  3211  3reeanv  3214  reuxfr1d  3733  reuind  3736  iuncom4  4976  dfiun2gOLD  5007  iunxiun  5073  inuni  5320  xpiundi  5725  xpiundir  5726  imaco  6240  coiun  6245  abrexco  7236  imaiun  7237  isomin  7330  isoini  7331  imaeqsexvOLD  7356  imaeqexov  7645  oarec  8574  mapsnend  9050  unfi  9185  brttrcl2  9728  genpass  11023  4fvwrd4  13665  4sqlem12  16976  imasleval  17555  lsmspsn  21042  utoptop  24173  metrest  24463  metust  24497  cfilucfil  24498  metuel2  24504  sleadd1  27948  addsuniflem  27960  addsasslem1  27962  addsasslem2  27963  addsdilem1  28106  0reno  28400  renegscl  28401  readdscl  28402  remulscl  28405  istrkg2ld  28439  axsegcon  28906  fusgreg2wsp  30317  nmoo0  30772  nmop0  31967  nmfn0  31968  rexunirn  32473  dmrab  32478  iunrnmptss  32546  ressupprn  32667  ordtconnlem1  33955  dya2icoseg2  34310  dya2iocnei  34314  omssubaddlem  34331  omssubadd  34332  satfvsuclem2  35382  satf0  35394  satffunlem1lem2  35425  satffunlem2lem2  35428  rexxfr3dALT  35661  bj-mpomptALT  37137  mptsnunlem  37356  fvineqsneq  37430  rabiun  37617  iundif1  37618  poimir  37677  ismblfin  37685  eldmqs1cossres  38677  erimeq2  38696  prter2  38899  prter3  38900  islshpat  39035  lshpsmreu  39127  islpln5  39554  islvol5  39598  cdlemftr3  40584  dvhb1dimN  41005  dib1dim  41184  mapdpglem3  41694  hdmapglem7a  41946  diophrex  42798  dfsclnbgr6  47871  r19.41dv  48781  reuxfr1dd  48785