Theorem rspc2ev 3564

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  rspc3ev  3566  opelxp  5616  fprb  7051  f1prex  7136  nf1const  7156  rspceov  7302  erov  8561  ralxpmap  8642  2dom  8774  elfiun  9119  dffi3  9120  ixpiunwdom  9279  1re  10906  hashdmpropge2  14125  wrdl2exs2  14587  ello12r  15154  ello1d  15160  elo12r  15165  o1lo1  15174  addcn2  15231  mulcn2  15233  bezoutlem3  16177  bezout  16179  pythagtriplem18  16461  pczpre  16476  pcdiv  16481  4sqlem3  16579  4sqlem4  16581  4sqlem12  16585  vdwlem1  16610  vdwlem6  16615  vdwlem8  16617  vdwlem12  16621  vdwlem13  16622  0ram  16649  ramz2  16653  cat1lem  17727  sgrp2rid2ex  18481  pmtr3ncom  18998  psgnunilem1  19016  irredn0  19860  isnzr2  20447  hausnei2  22412  cnhaus  22413  dishaus  22441  ordthauslem  22442  txuni2  22624  xkoopn  22648  txopn  22661  txdis  22691  txdis1cn  22694  pthaus  22697  txhaus  22706  tx1stc  22709  xkohaus  22712  regr1lem  22798  qustgplem  23180  methaus  23582  met2ndci  23584  metnrmlem3  23930  elplyr  25267  aaliou2b  25406  aaliou3lem9  25415  2irrexpq  25790  2irrexpqALT  25855  2sqlem2  26471  2sqlem8  26479  2sqlem11  26482  2sqb  26485  2sqnn0  26491  2sqnn  26492  pntibnd  26646  legov  26850  iscgrad  27076  f1otrge  27137  axsegconlem1  27188  axsegcon  27198  axpaschlem  27211  axlowdimlem6  27218  axlowdim1  27230  axlowdim2  27231  axeuclidlem  27233  umgrvad2edg  27483  wwlksnwwlksnon  28181  upgr4cycl4dv4e  28450  3cyclfrgrrn1  28550  4cycl2vnunb  28555  br8d  30851  lt2addrd  30976  xlt2addrd  30983  xrnarchi  31340  txomap  31686  tpr2rico  31764  qqhval2  31832  elsx  32062  isanmbfm  32123  br2base  32136  dya2iocnrect  32148  connpconn  33097  satfv1fvfmla1  33285  br8  33629  br4  33631  madecut  33992  brsegle  34337  hilbert1.1  34383  nn0prpwlem  34438  knoppndvlem21  34639  poimirlem1  35705  itg2addnclem3  35757  cntotbnd  35881  smprngopr  36137  3dim2  37409  llni2  37453  lvoli3  37518  lvoli2  37522  islinei  37681  psubspi2N  37689  elpaddri  37743  2rspcedvdw  40108  eldioph2lem1  40498  diophin  40510  fphpdo  40555  irrapxlem3  40562  irrapxlem4  40563  pellexlem6  40572  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell1234qrdich  40599  pell1qr1  40609  pellqrexplicit  40615  rmxycomplete  40655  dgraalem  40886  clsk3nimkb  41539  fourierdlem64  43601  rspceaov  44576  ichnreuop  44812  prelspr  44826  reuopreuprim  44866  6gbe  45111  7gbow  45112  8gbe  45113  9gbo  45114  11gbo  45115  modn0mul  45754  elbigo2r  45787  rrx2xpref1o  45952  inlinecirc02plem  46020  sepfsepc  46109  iscnrm3lem7  46121