Theorem r19.41v 3195

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.42v  3197  r19.41vv  3233  3reeanv  3236  reuxfr1d  3772  reuind  3775  iuncom4  5023  dfiun2gOLD  5054  iunxiun  5120  inuni  5368  xpiundi  5770  xpiundir  5771  imaco  6282  coiun  6287  abrexco  7281  imaiun  7282  isomin  7373  isoini  7374  imaeqsexvOLD  7399  imaeqexov  7688  oarec  8618  mapsnend  9101  unfi  9238  brttrcl2  9783  genpass  11078  4fvwrd4  13705  4sqlem12  17003  imasleval  17601  lsmspsn  21106  utoptop  24264  metrest  24558  metust  24592  cfilucfil  24593  metuel2  24599  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  addsdilem1  28195  0reno  28447  renegscl  28448  readdscl  28449  remulscl  28452  istrkg2ld  28486  axsegcon  28960  fusgreg2wsp  30368  nmoo0  30823  nmop0  32018  nmfn0  32019  rexunirn  32520  dmrab  32525  iunrnmptss  32588  ressupprn  32702  ordtconnlem1  33870  dya2icoseg2  34243  dya2iocnei  34247  omssubaddlem  34264  omssubadd  34265  satfvsuclem2  35328  satf0  35340  satffunlem1lem2  35371  satffunlem2lem2  35374  rexxfr3dALT  35607  bj-mpomptALT  37085  mptsnunlem  37304  fvineqsneq  37378  rabiun  37553  iundif1  37554  poimir  37613  ismblfin  37621  eldmqs1cossres  38615  erimeq2  38634  prter2  38837  prter3  38838  islshpat  38973  lshpsmreu  39065  islpln5  39492  islvol5  39536  cdlemftr3  40522  dvhb1dimN  40943  dib1dim  41122  mapdpglem3  41632  hdmapglem7a  41884  diophrex  42731  dfsclnbgr6  47730  r19.41dv  48535