Theorem rspc2ev 3624

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  2rspcedvdw  3625  rspc3ev  3628  opelxp  5712  fprb  7192  f1prex  7279  nf1const  7299  rspceov  7453  erov  8805  ralxpmap  8887  2dom  9027  elfiun  9422  dffi3  9423  ixpiunwdom  9582  1re  11211  hashdmpropge2  14441  wrdl2exs2  14894  ello12r  15458  ello1d  15464  elo12r  15469  o1lo1  15478  addcn2  15535  mulcn2  15537  bezoutlem3  16480  bezout  16482  pythagtriplem18  16762  pczpre  16777  pcdiv  16782  4sqlem3  16880  4sqlem4  16882  4sqlem12  16886  vdwlem1  16911  vdwlem6  16916  vdwlem8  16918  vdwlem12  16922  vdwlem13  16923  0ram  16950  ramz2  16954  cat1lem  18043  sgrp2rid2ex  18805  pmtr3ncom  19338  psgnunilem1  19356  irredn0  20230  isnzr2  20290  hausnei2  22849  cnhaus  22850  dishaus  22878  ordthauslem  22879  txuni2  23061  xkoopn  23085  txopn  23098  txdis  23128  txdis1cn  23131  pthaus  23134  txhaus  23143  tx1stc  23146  xkohaus  23149  regr1lem  23235  qustgplem  23617  methaus  24021  met2ndci  24023  metnrmlem3  24369  elplyr  25707  aaliou2b  25846  aaliou3lem9  25855  2irrexpq  26230  2irrexpqALT  26295  2sqlem2  26911  2sqlem8  26919  2sqlem11  26922  2sqb  26925  2sqnn0  26931  2sqnn  26932  pntibnd  27086  madecut  27367  mulsproplem12  27573  precsexlem11  27653  legov  27826  iscgrad  28052  f1otrge  28113  axsegconlem1  28165  axsegcon  28175  axpaschlem  28188  axlowdimlem6  28195  axlowdim1  28207  axlowdim2  28208  axeuclidlem  28210  umgrvad2edg  28460  wwlksnwwlksnon  29159  upgr4cycl4dv4e  29428  3cyclfrgrrn1  29528  4cycl2vnunb  29533  br8d  31827  lt2addrd  31952  xlt2addrd  31959  xrnarchi  32318  txomap  32803  tpr2rico  32881  qqhval2  32951  elsx  33181  br2base  33257  dya2iocnrect  33269  connpconn  34215  satfv1fvfmla1  34403  br8  34715  br4  34717  brsegle  35069  hilbert1.1  35115  nn0prpwlem  35196  knoppndvlem21  35397  poimirlem1  36478  itg2addnclem3  36530  cntotbnd  36653  smprngopr  36909  3dim2  38328  llni2  38372  lvoli3  38437  lvoli2  38441  islinei  38600  psubspi2N  38608  elpaddri  38662  eldioph2lem1  41484  diophin  41496  fphpdo  41541  irrapxlem3  41548  irrapxlem4  41549  pellexlem6  41558  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell1234qrdich  41585  pell1qr1  41595  pellqrexplicit  41601  rmxycomplete  41642  dgraalem  41873  tfsconcatrev  42084  clsk3nimkb  42777  fourierdlem64  44873  rspceaov  45892  ichnreuop  46127  prelspr  46141  reuopreuprim  46181  6gbe  46426  7gbow  46427  8gbe  46428  9gbo  46429  11gbo  46430  modn0mul  47160  elbigo2r  47193  rrx2xpref1o  47358  inlinecirc02plem  47426  sepfsepc  47514  iscnrm3lem7  47526