Theorem r19.41v 3168

Description: Restricted quantifier version 19.41v 1951. Version of r19.41 3242 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 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1850	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1951	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3063	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 628	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.42v  3170  r19.41vv  3208  3reeanv  3211  reuxfr1d  3697  reuind  3700  iuncom4  4943  iunxiun  5040  inuni  5287  xpiundi  5695  xpiundir  5696  imaco  6209  coiun  6215  abrexco  7192  imaiun  7193  isomin  7285  isoini  7286  imaeqsexvOLD  7311  imaeqexov  7598  oarec  8490  mapsnend  8976  unfi  9098  brttrcl2  9626  genpass  10923  4fvwrd4  13593  4sqlem12  16918  imasleval  17496  lsmspsn  21071  utoptop  24209  metrest  24499  metust  24533  cfilucfil  24534  metuel2  24540  leadds1  27995  addsuniflem  28007  addsasslem1  28009  addsasslem2  28010  addsdilem1  28157  elreno2  28501  renegscl  28504  readdscl  28505  remulscl  28508  istrkg2ld  28542  axsegcon  29010  fusgreg2wsp  30421  nmoo0  30877  nmop0  32072  nmfn0  32073  rexunirn  32576  dmrab  32581  iunrnmptss  32650  ressupprn  32778  ordtconnlem1  34084  dya2icoseg2  34438  dya2iocnei  34442  omssubaddlem  34459  omssubadd  34460  r1omhf  35265  satfvsuclem2  35558  satf0  35570  satffunlem1lem2  35601  satffunlem2lem2  35604  rexxfr3dALT  35837  bj-mpomptALT  37447  mptsnunlem  37668  fvineqsneq  37742  rabiun  37928  iundif1  37929  poimir  37988  ismblfin  37996  eldmqs1cossres  39079  erimeq2  39098  prter2  39341  prter3  39342  islshpat  39477  lshpsmreu  39569  islpln5  39995  islvol5  40039  cdlemftr3  41025  dvhb1dimN  41446  dib1dim  41625  mapdpglem3  42135  hdmapglem7a  42387  diophrex  43221  dfsclnbgr6  48346  r19.41dv  49289  reuxfr1dd  49294