Theorem rspc2ev 3578

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2ev	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
2	1	rspcev 3565	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 618	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1115	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3162	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3565	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ 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  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  2rspcedvdw  3579  opelxp  5667  fprb  7149  f1prex  7239  nf1const  7259  rspceov  7416  erov  8761  ralxpmap  8844  2dom  8977  elfiun  9343  dffi3  9344  ixpiunwdom  9505  1re  11144  hashdmpropge2  14445  wrdl2exs2  14908  ello12r  15479  ello1d  15485  elo12r  15490  o1lo1  15499  addcn2  15556  mulcn2  15558  bezoutlem3  16510  bezout  16512  pythagtriplem18  16803  pczpre  16818  pcdiv  16823  4sqlem3  16921  4sqlem4  16923  4sqlem12  16927  vdwlem1  16952  vdwlem6  16957  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  0ram  16991  ramz2  16995  cat1lem  18063  sgrp2rid2ex  18898  pmtr3ncom  19450  psgnunilem1  19468  irredn0  20403  isnzr2  20495  hausnei2  23318  cnhaus  23319  dishaus  23347  ordthauslem  23348  txuni2  23530  xkoopn  23554  txopn  23567  txdis  23597  txdis1cn  23600  pthaus  23603  txhaus  23612  tx1stc  23615  xkohaus  23618  regr1lem  23704  qustgplem  24086  methaus  24485  met2ndci  24487  metnrmlem3  24827  elplyr  26166  aaliou2b  26307  aaliou3lem9  26316  2irrexpq  26695  2irrexpqALT  26764  2sqlem2  27381  2sqlem8  27389  2sqlem11  27392  2sqb  27395  2sqnn0  27401  2sqnn  27402  pntibnd  27556  madecut  27875  mulsproplem12  28119  precsexlem11  28209  eucliddivs  28368  elz12si  28465  zz12s  28467  remulscllem1  28492  legov  28653  iscgrad  28879  f1otrge  28940  axsegconlem1  28986  axsegcon  28996  axpaschlem  29009  axlowdimlem6  29016  axlowdim1  29028  axlowdim2  29029  axeuclidlem  29031  umgrvad2edg  29282  wwlksnwwlksnon  29983  upgr4cycl4dv4e  30255  3cyclfrgrrn1  30355  4cycl2vnunb  30360  br8d  32681  lt2addrd  32823  xlt2addrd  32832  xrnarchi  33245  txomap  33978  tpr2rico  34056  qqhval2  34126  elsx  34338  br2base  34413  dya2iocnrect  34425  connpconn  35417  satfv1fvfmla1  35605  br8  35938  br4  35940  brsegle  36290  hilbert1.1  36336  nn0prpwlem  36504  knoppndvlem21  36792  poimirlem1  37942  itg2addnclem3  37994  cntotbnd  38117  smprngopr  38373  3dim2  39914  llni2  39958  lvoli3  40023  lvoli2  40027  islinei  40186  psubspi2N  40194  elpaddri  40248  eldioph2lem1  43192  diophin  43204  fphpdo  43245  irrapxlem3  43252  irrapxlem4  43253  pellexlem6  43262  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell1qr1  43299  pellqrexplicit  43305  rmxycomplete  43345  dgraalem  43573  tfsconcatrev  43776  clsk3nimkb  44467  fourierdlem64  46598  rspceaov  47639  modn0mul  47805  ichnreuop  47926  prelspr  47940  reuopreuprim  47980  6gbe  48241  7gbow  48242  8gbe  48243  9gbo  48244  11gbo  48245  elbigo2r  49023  rrx2xpref1o  49188  inlinecirc02plem  49256  sepfsepc  49397  iscnrm3lem7  49408