Theorem r19.41v 3166

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  r19.42v  3168  r19.41vv  3206  3reeanv  3209  reuxfr1d  3708  reuind  3711  iuncom4  4955  iunxiun  5052  inuni  5295  xpiundi  5695  xpiundir  5696  imaco  6209  coiun  6215  abrexco  7190  imaiun  7191  isomin  7283  isoini  7284  imaeqsexvOLD  7309  imaeqexov  7596  oarec  8489  mapsnend  8973  unfi  9095  brttrcl2  9623  genpass  10920  4fvwrd4  13564  4sqlem12  16884  imasleval  17462  lsmspsn  21036  utoptop  24178  metrest  24468  metust  24502  cfilucfil  24503  metuel2  24509  leadds1  27985  addsuniflem  27997  addsasslem1  27999  addsasslem2  28000  addsdilem1  28147  elreno2  28491  renegscl  28494  readdscl  28495  remulscl  28498  istrkg2ld  28532  axsegcon  29000  fusgreg2wsp  30411  nmoo0  30866  nmop0  32061  nmfn0  32062  rexunirn  32566  dmrab  32571  iunrnmptss  32640  ressupprn  32769  ordtconnlem1  34081  dya2icoseg2  34435  dya2iocnei  34439  omssubaddlem  34456  omssubadd  34457  r1omhf  35262  satfvsuclem2  35554  satf0  35566  satffunlem1lem2  35597  satffunlem2lem2  35600  rexxfr3dALT  35833  bj-mpomptALT  37324  mptsnunlem  37543  fvineqsneq  37617  rabiun  37794  iundif1  37795  poimir  37854  ismblfin  37862  eldmqs1cossres  38918  erimeq2  38937  prter2  39141  prter3  39142  islshpat  39277  lshpsmreu  39369  islpln5  39795  islvol5  39839  cdlemftr3  40825  dvhb1dimN  41246  dib1dim  41425  mapdpglem3  41935  hdmapglem7a  42187  diophrex  43017  dfsclnbgr6  48104  r19.41dv  49047  reuxfr1dd  49052