Theorem r19.41v 3197

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  r19.42v  3199  r19.41vv  3237  3reeanv  3240  reuxfr1d  3715  reuind  3718  iuncom4  4967  iunxiun  5065  inuni  5322  xpiundi  5734  xpiundir  5735  imaco  6254  coiun  6260  abrexco  7244  imaiun  7245  isomin  7341  isoini  7342  imaeqexov  7654  oarec  8549  mapsnend  9036  unfi  9158  brttrcl2  9686  genpass  11005  4fvwrd4  13688  4sqlem12  17033  imasleval  17612  lsmspsn  21234  utoptop  24420  metrest  24710  metust  24744  cfilucfil  24745  metuel2  24751  leadds1  28211  addsuniflem  28223  addsasslem1  28225  addsasslem2  28226  addsdilem1  28373  elreno2  28717  renegscl  28720  readdscl  28721  remulscl  28724  istrkg2ld  28758  axsegcon  29306  fusgreg2wsp  30716  nmoo0  31172  nmop0  32367  nmfn0  32368  rexunirn  32867  dmrab  32872  iunrnmptss  32939  ressupprn  33064  ordtconnlem1  34337  dya2icoseg2  34692  dya2iocnei  34696  omssubaddlem  34713  omssubadd  34714  r1omhf  35517  vonf1oonfo  35615  satfvsuclem2  35865  satf0  35877  satffunlem1lem2  35908  satffunlem2lem2  35911  rexxfr3dALT  36144  bj-mpomptALT  37794  mptsnunlem  38017  fvineqsneq  38091  rabiun  38277  iundif1  38278  poimir  38337  ismblfin  38345  eldmqs1cossres  39426  erimeq2  39445  prter2  39688  prter3  39689  islshpat  39824  lshpsmreu  39916  islpln5  40342  islvol5  40386  cdlemftr3  41372  dvhb1dimN  41793  dib1dim  41972  mapdpglem3  42482  hdmapglem7a  42734  diophrex  43539  dfsclnbgr6  48656  r19.41dv  49613  reuxfr1dd  49618