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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3052  df-rex 3061

This theorem is referenced by:  2rspcedvdw  3621  rspc3ev  3624  opelxp  5713  fprb  7204  f1prex  7291  nf1const  7310  rspceov  7465  erov  8831  ralxpmap  8913  2dom  9053  elfiun  9453  dffi3  9454  ixpiunwdom  9613  1re  11244  hashdmpropge2  14477  wrdl2exs2  14930  ello12r  15494  ello1d  15500  elo12r  15505  o1lo1  15514  addcn2  15571  mulcn2  15573  bezoutlem3  16517  bezout  16519  pythagtriplem18  16801  pczpre  16816  pcdiv  16821  4sqlem3  16919  4sqlem4  16921  4sqlem12  16925  vdwlem1  16950  vdwlem6  16955  vdwlem8  16957  vdwlem12  16961  vdwlem13  16962  0ram  16989  ramz2  16993  cat1lem  18085  sgrp2rid2ex  18884  pmtr3ncom  19435  psgnunilem1  19453  irredn0  20367  isnzr2  20462  hausnei2  23288  cnhaus  23289  dishaus  23317  ordthauslem  23318  txuni2  23500  xkoopn  23524  txopn  23537  txdis  23567  txdis1cn  23570  pthaus  23573  txhaus  23582  tx1stc  23585  xkohaus  23588  regr1lem  23674  qustgplem  24056  methaus  24460  met2ndci  24462  metnrmlem3  24808  elplyr  26166  aaliou2b  26307  aaliou3lem9  26316  2irrexpq  26696  2irrexpqALT  26763  2sqlem2  27382  2sqlem8  27390  2sqlem11  27393  2sqb  27396  2sqnn0  27402  2sqnn  27403  pntibnd  27557  madecut  27840  mulsproplem12  28062  precsexlem11  28150  remulscllem1  28285  legov  28446  iscgrad  28672  f1otrge  28733  axsegconlem1  28785  axsegcon  28795  axpaschlem  28808  axlowdimlem6  28815  axlowdim1  28827  axlowdim2  28828  axeuclidlem  28830  umgrvad2edg  29083  wwlksnwwlksnon  29783  upgr4cycl4dv4e  30052  3cyclfrgrrn1  30152  4cycl2vnunb  30157  br8d  32458  lt2addrd  32582  xlt2addrd  32589  xrnarchi  32960  txomap  33522  tpr2rico  33600  qqhval2  33670  elsx  33900  br2base  33976  dya2iocnrect  33988  connpconn  34932  satfv1fvfmla1  35120  br8  35437  br4  35439  brsegle  35791  hilbert1.1  35837  nn0prpwlem  35893  knoppndvlem21  36094  poimirlem1  37181  itg2addnclem3  37233  cntotbnd  37356  smprngopr  37612  3dim2  39027  llni2  39071  lvoli3  39136  lvoli2  39140  islinei  39299  psubspi2N  39307  elpaddri  39361  eldioph2lem1  42262  diophin  42274  fphpdo  42319  irrapxlem3  42326  irrapxlem4  42327  pellexlem6  42336  pell1234qrreccl  42356  pell1234qrmulcl  42357  pell1234qrdich  42363  pell1qr1  42373  pellqrexplicit  42379  rmxycomplete  42420  dgraalem  42651  tfsconcatrev  42859  clsk3nimkb  43552  fourierdlem64  45638  rspceaov  46657  ichnreuop  46891  prelspr  46905  reuopreuprim  46945  6gbe  47190  7gbow  47191  8gbe  47192  9gbo  47193  11gbo  47194  modn0mul  47721  elbigo2r  47754  rrx2xpref1o  47919  inlinecirc02plem  47987  sepfsepc  48074  iscnrm3lem7  48086