Theorem r19.41v 3192

Description: Restricted quantifier version 19.41v 1981. Version of r19.41 3266 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 3087	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 474	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1880	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1981	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3087	. . . 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 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.42v  3194  r19.41vv  3232  3reeanv  3235  reuxfr1d  3707  reuind  3710  iuncom4  4959  iunxiun  5056  inuni  5310  xpiundi  5721  xpiundir  5722  imaco  6252  coiun  6258  abrexco  7249  imaiun  7250  isomin  7346  isoini  7347  imaeqexov  7660  mpt3mpt  7686  oarec  8574  mapsnend  9068  unfi  9190  brttrcl2  9719  genpass  11098  4fvwrd4  13786  4sqlem12  17140  imasleval  17719  lsmspsn  21365  utoptop  24559  metrest  24849  metust  24883  cfilucfil  24884  metuel2  24890  leadds1  28381  addsuniflem  28393  addsasslem1  28395  addsasslem2  28396  addsdilem1  28543  elreno2  28887  renegscl  28890  readdscl  28891  remulscl  28894  istrkg2ld  28928  axsegcon  29511  fusgreg2wsp  30943  nmoo0  31399  nmop0  32594  nmfn0  32595  rexunirn  33136  dmrab  33141  iunrnmptss  33207  ressupprn  33331  ordtconnlem1  34603  dya2icoseg2  34957  dya2iocnei  34961  omssubaddlem  34978  omssubadd  34979  vonf1oonfo  35969  satfvsuclem2  36212  satf0  36224  satffunlem1lem2  36255  satffunlem2lem2  36258  rexxfr3dALT  36491  bj-mpomptALT  38134  mptsnunlem  38355  fvineqsneq  38429  rabiun  38615  iundif1  38616  poimir  38665  ismblfin  38673  eldmqs1cossres  39770  erimeq2  39789  prter2  40032  prter3  40033  islshpat  40168  lshpsmreu  40260  islpln5  40686  islvol5  40730  cdlemftr3  41716  dvhb1dimN  42137  dib1dim  42316  mapdpglem3  42826  hdmapglem7a  43078  diophrex  43880  dfsclnbgr6  49050  r19.41dv  50006  reuxfr1dd  50011