Theorem rspc2ev 3620

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066

This theorem is referenced by:  2rspcedvdw  3621  rspc3ev  3624  opelxp  5708  fprb  7200  f1prex  7287  nf1const  7307  rspceov  7461  erov  8824  ralxpmap  8906  2dom  9046  elfiun  9445  dffi3  9446  ixpiunwdom  9605  1re  11236  hashdmpropge2  14468  wrdl2exs2  14921  ello12r  15485  ello1d  15491  elo12r  15496  o1lo1  15505  addcn2  15562  mulcn2  15564  bezoutlem3  16508  bezout  16510  pythagtriplem18  16792  pczpre  16807  pcdiv  16812  4sqlem3  16910  4sqlem4  16912  4sqlem12  16916  vdwlem1  16941  vdwlem6  16946  vdwlem8  16948  vdwlem12  16952  vdwlem13  16953  0ram  16980  ramz2  16984  cat1lem  18076  sgrp2rid2ex  18870  pmtr3ncom  19421  psgnunilem1  19439  irredn0  20351  isnzr2  20446  hausnei2  23244  cnhaus  23245  dishaus  23273  ordthauslem  23274  txuni2  23456  xkoopn  23480  txopn  23493  txdis  23523  txdis1cn  23526  pthaus  23529  txhaus  23538  tx1stc  23541  xkohaus  23544  regr1lem  23630  qustgplem  24012  methaus  24416  met2ndci  24418  metnrmlem3  24764  elplyr  26122  aaliou2b  26263  aaliou3lem9  26272  2irrexpq  26652  2irrexpqALT  26719  2sqlem2  27338  2sqlem8  27346  2sqlem11  27349  2sqb  27352  2sqnn0  27358  2sqnn  27359  pntibnd  27513  madecut  27796  mulsproplem12  28014  precsexlem11  28102  remulscllem1  28215  legov  28376  iscgrad  28602  f1otrge  28663  axsegconlem1  28715  axsegcon  28725  axpaschlem  28738  axlowdimlem6  28745  axlowdim1  28757  axlowdim2  28758  axeuclidlem  28760  umgrvad2edg  29013  wwlksnwwlksnon  29713  upgr4cycl4dv4e  29982  3cyclfrgrrn1  30082  4cycl2vnunb  30087  br8d  32383  lt2addrd  32505  xlt2addrd  32512  xrnarchi  32870  txomap  33371  tpr2rico  33449  qqhval2  33519  elsx  33749  br2base  33825  dya2iocnrect  33837  connpconn  34781  satfv1fvfmla1  34969  br8  35286  br4  35288  brsegle  35640  hilbert1.1  35686  nn0prpwlem  35742  knoppndvlem21  35943  poimirlem1  37029  itg2addnclem3  37081  cntotbnd  37204  smprngopr  37460  3dim2  38878  llni2  38922  lvoli3  38987  lvoli2  38991  islinei  39150  psubspi2N  39158  elpaddri  39212  eldioph2lem1  42102  diophin  42114  fphpdo  42159  irrapxlem3  42166  irrapxlem4  42167  pellexlem6  42176  pell1234qrreccl  42196  pell1234qrmulcl  42197  pell1234qrdich  42203  pell1qr1  42213  pellqrexplicit  42219  rmxycomplete  42260  dgraalem  42491  tfsconcatrev  42700  clsk3nimkb  43393  fourierdlem64  45481  rspceaov  46500  ichnreuop  46735  prelspr  46749  reuopreuprim  46789  6gbe  47034  7gbow  47035  8gbe  47036  9gbo  47037  11gbo  47038  modn0mul  47516  elbigo2r  47549  rrx2xpref1o  47714  inlinecirc02plem  47782  sepfsepc  47869  iscnrm3lem7  47881