Theorem rspc2ev 3590

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062

This theorem is referenced by:  2rspcedvdw  3591  rspc3ev  3594  opelxp  5661  fprb  7142  f1prex  7232  nf1const  7252  rspceov  7409  erov  8755  ralxpmap  8838  2dom  8971  elfiun  9337  dffi3  9338  ixpiunwdom  9499  1re  11136  hashdmpropge2  14410  wrdl2exs2  14873  ello12r  15444  ello1d  15450  elo12r  15455  o1lo1  15464  addcn2  15521  mulcn2  15523  bezoutlem3  16472  bezout  16474  pythagtriplem18  16764  pczpre  16779  pcdiv  16784  4sqlem3  16882  4sqlem4  16884  4sqlem12  16888  vdwlem1  16913  vdwlem6  16918  vdwlem8  16920  vdwlem12  16924  vdwlem13  16925  0ram  16952  ramz2  16956  cat1lem  18024  sgrp2rid2ex  18856  pmtr3ncom  19408  psgnunilem1  19426  irredn0  20363  isnzr2  20455  hausnei2  23301  cnhaus  23302  dishaus  23330  ordthauslem  23331  txuni2  23513  xkoopn  23537  txopn  23550  txdis  23580  txdis1cn  23583  pthaus  23586  txhaus  23595  tx1stc  23598  xkohaus  23601  regr1lem  23687  qustgplem  24069  methaus  24468  met2ndci  24470  metnrmlem3  24810  elplyr  26166  aaliou2b  26309  aaliou3lem9  26318  2irrexpq  26700  2irrexpqALT  26770  2sqlem2  27389  2sqlem8  27397  2sqlem11  27400  2sqb  27403  2sqnn0  27409  2sqnn  27410  pntibnd  27564  madecut  27865  mulsproplem12  28109  precsexlem11  28198  eucliddivs  28355  elzs12i  28452  zzs12  28454  remulscllem1  28479  legov  28640  iscgrad  28866  f1otrge  28927  axsegconlem1  28973  axsegcon  28983  axpaschlem  28996  axlowdimlem6  29003  axlowdim1  29015  axlowdim2  29016  axeuclidlem  29018  umgrvad2edg  29269  wwlksnwwlksnon  29971  upgr4cycl4dv4e  30243  3cyclfrgrrn1  30343  4cycl2vnunb  30348  br8d  32668  lt2addrd  32811  xlt2addrd  32820  xrnarchi  33247  txomap  33972  tpr2rico  34050  qqhval2  34120  elsx  34332  br2base  34407  dya2iocnrect  34419  connpconn  35410  satfv1fvfmla1  35598  br8  35931  br4  35933  brsegle  36283  hilbert1.1  36329  nn0prpwlem  36497  knoppndvlem21  36707  poimirlem1  37793  itg2addnclem3  37845  cntotbnd  37968  smprngopr  38224  3dim2  39765  llni2  39809  lvoli3  39874  lvoli2  39878  islinei  40037  psubspi2N  40045  elpaddri  40099  eldioph2lem1  43038  diophin  43050  fphpdo  43095  irrapxlem3  43102  irrapxlem4  43103  pellexlem6  43112  pell1234qrreccl  43132  pell1234qrmulcl  43133  pell1234qrdich  43139  pell1qr1  43149  pellqrexplicit  43155  rmxycomplete  43195  dgraalem  43423  tfsconcatrev  43626  clsk3nimkb  44317  fourierdlem64  46450  rspceaov  47479  modn0mul  47639  ichnreuop  47754  prelspr  47768  reuopreuprim  47808  6gbe  48053  7gbow  48054  8gbe  48055  9gbo  48056  11gbo  48057  elbigo2r  48835  rrx2xpref1o  49000  inlinecirc02plem  49068  sepfsepc  49209  iscnrm3lem7  49220