Theorem rspc2ev 3576

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  ∃wrex 3108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rex 3113  df-v 3442

This theorem is referenced by:  rspc3ev  3578  opelxp  5486  fprb  6830  f1prex  6912  rspceov  7069  erov  8251  ralxpmap  8316  2dom  8437  elfiun  8747  dffi3  8748  ixpiunwdom  8908  1re  10494  hashdmpropge2  13691  wrdl2exs2  14148  ello12r  14712  ello1d  14718  elo12r  14723  o1lo1  14732  addcn2  14788  mulcn2  14790  bezoutlem3  15722  bezout  15724  pythagtriplem18  16002  pczpre  16017  pcdiv  16022  4sqlem3  16119  4sqlem4  16121  4sqlem12  16125  vdwlem1  16150  vdwlem6  16155  vdwlem8  16157  vdwlem12  16161  vdwlem13  16162  0ram  16189  ramz2  16193  sgrp2rid2ex  17857  pmtr3ncom  18338  psgnunilem1  18356  irredn0  19147  isnzr2  19729  hausnei2  21649  cnhaus  21650  dishaus  21678  ordthauslem  21679  txuni2  21861  xkoopn  21885  txopn  21898  txdis  21928  txdis1cn  21931  pthaus  21934  txhaus  21943  tx1stc  21946  xkohaus  21949  regr1lem  22035  qustgplem  22416  methaus  22817  met2ndci  22819  metnrmlem3  23156  elplyr  24478  aaliou2b  24617  aaliou3lem9  24626  2irrexpq  24998  2irrexpqALT  25063  2sqlem2  25680  2sqlem8  25688  2sqlem11  25691  2sqb  25694  2sqnn0  25700  2sqnn  25701  pntibnd  25855  legov  26057  iscgrad  26283  f1otrge  26345  axsegconlem1  26390  axsegcon  26400  axpaschlem  26413  axlowdimlem6  26420  axlowdim1  26432  axlowdim2  26433  axeuclidlem  26435  umgrvad2edg  26682  wwlksnwwlksnon  27380  upgr4cycl4dv4e  27650  3cyclfrgrrn1  27752  4cycl2vnunb  27757  br8d  30047  lt2addrd  30159  xlt2addrd  30166  xrnarchi  30447  txomap  30711  tpr2rico  30768  qqhval2  30836  elsx  31066  isanmbfm  31127  br2base  31140  dya2iocnrect  31152  connpconn  32092  satfv1fvfmla1  32280  br8  32602  br4  32604  brsegle  33180  hilbert1.1  33226  nn0prpwlem  33281  knoppndvlem21  33482  poimirlem1  34445  itg2addnclem3  34497  cntotbnd  34627  smprngopr  34883  3dim2  36156  llni2  36200  lvoli3  36265  lvoli2  36269  islinei  36428  psubspi2N  36436  elpaddri  36490  eldioph2lem1  38863  diophin  38875  fphpdo  38920  irrapxlem3  38927  irrapxlem4  38928  pellexlem6  38937  pell1234qrreccl  38957  pell1234qrmulcl  38958  pell1234qrdich  38964  pell1qr1  38974  pellqrexplicit  38980  rmxycomplete  39020  dgraalem  39251  clsk3nimkb  39896  fourierdlem64  42019  rspceaov  42934  ichnreuop  43138  prelspr  43152  reuopreuprim  43192  6gbe  43440  7gbow  43441  8gbe  43442  9gbo  43443  11gbo  43444  modn0mul  44083  elbigo2r  44116  rrx2xpref1o  44208  inlinecirc02plem  44276