Theorem rspc2ev 3604

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 3591	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 617	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1114	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3158	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3591	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  2rspcedvdw  3605  rspc3ev  3608  opelxp  5676  fprb  7170  f1prex  7261  nf1const  7281  rspceov  7438  erov  8789  ralxpmap  8871  2dom  9003  elfiun  9387  dffi3  9388  ixpiunwdom  9549  1re  11180  hashdmpropge2  14454  wrdl2exs2  14918  ello12r  15489  ello1d  15495  elo12r  15500  o1lo1  15509  addcn2  15566  mulcn2  15568  bezoutlem3  16517  bezout  16519  pythagtriplem18  16809  pczpre  16824  pcdiv  16829  4sqlem3  16927  4sqlem4  16929  4sqlem12  16933  vdwlem1  16958  vdwlem6  16963  vdwlem8  16965  vdwlem12  16969  vdwlem13  16970  0ram  16997  ramz2  17001  cat1lem  18064  sgrp2rid2ex  18860  pmtr3ncom  19411  psgnunilem1  19429  irredn0  20338  isnzr2  20433  hausnei2  23246  cnhaus  23247  dishaus  23275  ordthauslem  23276  txuni2  23458  xkoopn  23482  txopn  23495  txdis  23525  txdis1cn  23528  pthaus  23531  txhaus  23540  tx1stc  23543  xkohaus  23546  regr1lem  23632  qustgplem  24014  methaus  24414  met2ndci  24416  metnrmlem3  24756  elplyr  26112  aaliou2b  26255  aaliou3lem9  26264  2irrexpq  26646  2irrexpqALT  26716  2sqlem2  27335  2sqlem8  27343  2sqlem11  27346  2sqb  27349  2sqnn0  27355  2sqnn  27356  pntibnd  27510  madecut  27800  mulsproplem12  28036  precsexlem11  28125  eucliddivs  28271  zzs12  28345  remulscllem1  28357  legov  28518  iscgrad  28744  f1otrge  28805  axsegconlem1  28850  axsegcon  28860  axpaschlem  28873  axlowdimlem6  28880  axlowdim1  28892  axlowdim2  28893  axeuclidlem  28895  umgrvad2edg  29146  wwlksnwwlksnon  29851  upgr4cycl4dv4e  30120  3cyclfrgrrn1  30220  4cycl2vnunb  30225  br8d  32544  lt2addrd  32680  xlt2addrd  32688  xrnarchi  33144  txomap  33830  tpr2rico  33908  qqhval2  33978  elsx  34190  br2base  34266  dya2iocnrect  34278  connpconn  35222  satfv1fvfmla1  35410  br8  35738  br4  35740  brsegle  36091  hilbert1.1  36137  nn0prpwlem  36305  knoppndvlem21  36515  poimirlem1  37610  itg2addnclem3  37662  cntotbnd  37785  smprngopr  38041  3dim2  39457  llni2  39501  lvoli3  39566  lvoli2  39570  islinei  39729  psubspi2N  39737  elpaddri  39791  eldioph2lem1  42741  diophin  42753  fphpdo  42798  irrapxlem3  42805  irrapxlem4  42806  pellexlem6  42815  pell1234qrreccl  42835  pell1234qrmulcl  42836  pell1234qrdich  42842  pell1qr1  42852  pellqrexplicit  42858  rmxycomplete  42899  dgraalem  43127  tfsconcatrev  43330  clsk3nimkb  44022  fourierdlem64  46161  rspceaov  47188  modn0mul  47348  ichnreuop  47463  prelspr  47477  reuopreuprim  47517  6gbe  47762  7gbow  47763  8gbe  47764  9gbo  47765  11gbo  47766  elbigo2r  48532  rrx2xpref1o  48697  inlinecirc02plem  48765  sepfsepc  48906  iscnrm3lem7  48917