Theorem r19.41v 3192

Description: Restricted quantifier version 19.41v 1982. 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 1881	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1982	. . 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 1812   ∈ wcel 2145  ∃wrex 3086

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 3087

This theorem is used by:  r19.42v  3194  r19.41vv  3232  3reeanv  3235  reuxfr1d  3708  reuind  3711  iuncom4  4960  iunxiun  5057  inuni  5314  xpiundi  5726  xpiundir  5727  imaco  6247  coiun  6253  abrexco  7241  imaiun  7242  isomin  7338  isoini  7339  imaeqexov  7652  oarec  8549  mapsnend  9043  unfi  9165  brttrcl2  9693  genpass  11018  4fvwrd4  13703  4sqlem12  17048  imasleval  17627  lsmspsn  21268  utoptop  24460  metrest  24750  metust  24784  cfilucfil  24785  metuel2  24791  leadds1  28254  addsuniflem  28266  addsasslem1  28268  addsasslem2  28269  addsdilem1  28416  elreno2  28760  renegscl  28763  readdscl  28764  remulscl  28767  istrkg2ld  28801  axsegcon  29384  fusgreg2wsp  30816  nmoo0  31272  nmop0  32467  nmfn0  32468  rexunirn  32967  dmrab  32972  iunrnmptss  33038  ressupprn  33162  ordtconnlem1  34434  dya2icoseg2  34789  dya2iocnei  34793  omssubaddlem  34810  omssubadd  34811  r1omhf  35614  vonf1oonfo  35712  satfvsuclem2  35939  satf0  35951  satffunlem1lem2  35982  satffunlem2lem2  35985  rexxfr3dALT  36218  bj-mpomptALT  37869  mptsnunlem  38092  fvineqsneq  38166  rabiun  38352  iundif1  38353  poimir  38402  ismblfin  38410  eldmqs1cossres  39492  erimeq2  39511  prter2  39754  prter3  39755  islshpat  39890  lshpsmreu  39982  islpln5  40408  islvol5  40452  cdlemftr3  41438  dvhb1dimN  41859  dib1dim  42038  mapdpglem3  42548  hdmapglem7a  42800  diophrex  43620  dfsclnbgr6  48774  r19.41dv  49730  reuxfr1dd  49735