Theorem rspc2ev 3070

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
rspc2v.2	|- ( y = B -> ( ch <-> ps ) )

Assertion

Ref	Expression
rspc2ev	|- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Distinct variable groups:   x, y, A   y, B   x, C   x, D, y   ch, x   ps, y

Allowed substitution hints:   ph( x, y)   ps( x)   ch( y)   B( x)   C( y)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 |- ( y = B -> ( ch <-> ps ) )
2	1	rspcev 3062	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 564	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1176	. 2 |- ( ( A e. C /\ B e. D /\ ps ) -> ( A e. C /\ E. y e. D ch ) )
5		rspc2v.1	. . . 4 |- ( x = A -> ( ph <-> ch ) )
6	5	rexbidv 2726	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3062	. 2 |- ( ( A e. C /\ E. y e. D ch ) -> E. x e. C E. y e. D ph )
8	4, 7	syl 16	1 |- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 958   = wceq 1362   e. wcel 1755   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-v 2964

This theorem is referenced by:  rspc3ev  3072  opelxp  4856  rspceov  6117  erov  7185  ralxpmap  7250  2dom  7370  elfiun  7668  dffi3  7669  ixpiunwdom  7794  1re  9372  ello12r  12978  ello1d  12984  elo12r  12989  o1lo1  12998  addcn2  13054  mulcn2  13056  bezoutlem3  13706  bezout  13708  pythagtriplem18  13881  pczpre  13896  pcdiv  13901  4sqlem3  13993  4sqlem4  13995  4sqlem12  13999  vdwlem1  14024  vdwlem6  14029  vdwlem8  14031  vdwlem12  14035  vdwlem13  14036  0ram  14063  ramz2  14067  pmtr3ncom  15960  psgnunilem1  15978  irredn0  16728  isnzr2  17266  hausnei2  18798  cnhaus  18799  dishaus  18827  ordthauslem  18828  txuni2  18979  xkoopn  19003  txopn  19016  txdis  19046  txdis1cn  19049  pthaus  19052  txhaus  19061  tx1stc  19064  xkohaus  19067  regr1lem  19153  divstgplem  19532  methaus  19936  met2ndci  19938  metnrmlem3  20278  elplyr  21553  aaliou2b  21691  aaliou3lem9  21700  2sqlem2  22587  2sqlem8  22595  2sqlem11  22598  2sqb  22601  pntibnd  22726  legov  22891  f1otrge  22940  axsegconlem1  22985  axsegcon  22995  axpaschlem  23008  axlowdimlem6  23015  axlowdim1  23027  axlowdim2  23028  axeuclidlem  23030  br8d  25765  lt2addrd  25860  xlt2addrd  25875  xrnarchi  26024  pstmfval  26176  tpr2rico  26195  qqhval2  26264  elsx  26461  isanmbfm  26524  br2base  26537  dya2iocnrect  26549  conpcon  26971  br8  27412  br4  27414  fprb  27430  brsegle  27985  hilbert1.1  28031  itg2addnclem3  28286  nn0prpwlem  28358  cntotbnd  28536  smprngopr  28693  eldioph2lem1  28940  diophin  28953  fphpdo  28998  irrapxlem3  29007  irrapxlem4  29008  pellexlem6  29017  pell1234qrreccl  29037  pell1234qrmulcl  29038  pell1234qrdich  29044  pell1qr1  29054  pellqrexplicit  29060  rmxycomplete  29100  dgraalem  29344  rspceaov  29946  el2wlksotot  30244  3cyclfrgrarn1  30447  4cycl2vnunb  30452  3dim2  32682  llni2  32726  lvoli3  32791  lvoli2  32795  islinei  32954  psubspi2N  32962  elpaddri  33016