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  7143  f1prex  7233  nf1const  7253  rspceov  7410  erov  8756  ralxpmap  8839  2dom  8972  elfiun  9338  dffi3  9339  ixpiunwdom  9500  1re  11137  hashdmpropge2  14411  wrdl2exs2  14874  ello12r  15445  ello1d  15451  elo12r  15456  o1lo1  15465  addcn2  15522  mulcn2  15524  bezoutlem3  16473  bezout  16475  pythagtriplem18  16765  pczpre  16780  pcdiv  16785  4sqlem3  16883  4sqlem4  16885  4sqlem12  16889  vdwlem1  16914  vdwlem6  16919  vdwlem8  16921  vdwlem12  16925  vdwlem13  16926  0ram  16953  ramz2  16957  cat1lem  18025  sgrp2rid2ex  18857  pmtr3ncom  19409  psgnunilem1  19427  irredn0  20364  isnzr2  20456  hausnei2  23302  cnhaus  23303  dishaus  23331  ordthauslem  23332  txuni2  23514  xkoopn  23538  txopn  23551  txdis  23581  txdis1cn  23584  pthaus  23587  txhaus  23596  tx1stc  23599  xkohaus  23602  regr1lem  23688  qustgplem  24070  methaus  24469  met2ndci  24471  metnrmlem3  24811  elplyr  26167  aaliou2b  26310  aaliou3lem9  26319  2irrexpq  26701  2irrexpqALT  26771  2sqlem2  27390  2sqlem8  27398  2sqlem11  27401  2sqb  27404  2sqnn0  27410  2sqnn  27411  pntibnd  27565  madecut  27884  mulsproplem12  28128  precsexlem11  28218  eucliddivs  28377  elz12si  28474  zz12s  28476  remulscllem1  28501  legov  28662  iscgrad  28888  f1otrge  28949  axsegconlem1  28995  axsegcon  29005  axpaschlem  29018  axlowdimlem6  29025  axlowdim1  29037  axlowdim2  29038  axeuclidlem  29040  umgrvad2edg  29291  wwlksnwwlksnon  29993  upgr4cycl4dv4e  30265  3cyclfrgrrn1  30365  4cycl2vnunb  30370  br8d  32690  lt2addrd  32833  xlt2addrd  32842  xrnarchi  33270  txomap  34004  tpr2rico  34082  qqhval2  34152  elsx  34364  br2base  34439  dya2iocnrect  34451  connpconn  35442  satfv1fvfmla1  35630  br8  35963  br4  35965  brsegle  36315  hilbert1.1  36361  nn0prpwlem  36529  knoppndvlem21  36745  poimirlem1  37835  itg2addnclem3  37887  cntotbnd  38010  smprngopr  38266  3dim2  39807  llni2  39851  lvoli3  39916  lvoli2  39920  islinei  40079  psubspi2N  40087  elpaddri  40141  eldioph2lem1  43080  diophin  43092  fphpdo  43137  irrapxlem3  43144  irrapxlem4  43145  pellexlem6  43154  pell1234qrreccl  43174  pell1234qrmulcl  43175  pell1234qrdich  43181  pell1qr1  43191  pellqrexplicit  43197  rmxycomplete  43237  dgraalem  43465  tfsconcatrev  43668  clsk3nimkb  44359  fourierdlem64  46491  rspceaov  47520  modn0mul  47680  ichnreuop  47795  prelspr  47809  reuopreuprim  47849  6gbe  48094  7gbow  48095  8gbe  48096  9gbo  48097  11gbo  48098  elbigo2r  48876  rrx2xpref1o  49041  inlinecirc02plem  49109  sepfsepc  49250  iscnrm3lem7  49261