Theorem r19.41v 3169

Description: Restricted quantifier version 19.41v 1956. Version of r19.41 3243 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 3064	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 469	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1855	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1956	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3064	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 225	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 633	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 300	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  r19.42v  3171  r19.41vv  3209  3reeanv  3212  reuxfr1d  3691  reuind  3694  iuncom4  4930  iunxiun  5026  inuni  5278  xpiundi  5689  xpiundir  5690  imaco  6202  coiun  6208  abrexco  7188  imaiun  7189  isomin  7281  isoini  7282  imaeqsexvOLD  7307  imaeqexov  7594  oarec  8487  mapsnend  8973  unfi  9095  brttrcl2  9626  genpass  10923  4fvwrd4  13593  4sqlem12  16918  imasleval  17496  lsmspsn  21074  utoptop  24217  metrest  24507  metust  24541  cfilucfil  24542  metuel2  24548  leadds1  27999  addsuniflem  28011  addsasslem1  28013  addsasslem2  28014  addsdilem1  28161  elreno2  28505  renegscl  28508  readdscl  28509  remulscl  28512  istrkg2ld  28546  axsegcon  29014  fusgreg2wsp  30424  nmoo0  30880  nmop0  32075  nmfn0  32076  rexunirn  32579  dmrab  32584  iunrnmptss  32654  ressupprn  32782  ordtconnlem1  34108  dya2icoseg2  34462  dya2iocnei  34466  omssubaddlem  34483  omssubadd  34484  r1omhf  35287  satfvsuclem2  35588  satf0  35600  satffunlem1lem2  35631  satffunlem2lem2  35634  rexxfr3dALT  35867  bj-mpomptALT  37477  mptsnunlem  37700  fvineqsneq  37774  rabiun  37960  iundif1  37961  poimir  38020  ismblfin  38028  eldmqs1cossres  39111  erimeq2  39130  prter2  39373  prter3  39374  islshpat  39509  lshpsmreu  39601  islpln5  40027  islvol5  40071  cdlemftr3  41057  dvhb1dimN  41478  dib1dim  41657  mapdpglem3  42167  hdmapglem7a  42419  diophrex  43224  dfsclnbgr6  48349  r19.41dv  49292  reuxfr1dd  49297