Theorem rspc2ev 3172

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 3161	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 577	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1211	. 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 2912	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3161	. 2 |- ( ( A e. C /\ E. y e. D ch ) -> E. x e. C E. y e. D ph )
8	4, 7	syl 17	1 |- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1454   e. wcel 1897   E.wrex 2749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rex 2754  df-v 3058

This theorem is referenced by:  rspc3ev  3174  opelxp  4882  f1prex  6206  rspceov  6353  erov  7485  ralxpmap  7546  2dom  7667  elfiun  7969  dffi3  7970  ixpiunwdom  8131  1re  9667  wrdl2exs2  13070  ello12r  13629  ello1d  13635  elo12r  13640  o1lo1  13649  addcn2  13705  mulcn2  13707  bezoutlem3OLD  14553  bezoutlem3  14556  bezout  14558  pythagtriplem18  14830  pczpre  14845  pcdiv  14850  4sqlem3  14942  4sqlem4  14944  4sqlem12  14948  vdwlem1  14979  vdwlem6  14984  vdwlem8  14986  vdwlem12  14990  vdwlem13  14991  0ram  15026  ramz2  15030  sgrp2rid2ex  16709  pmtr3ncom  17164  psgnunilem1  17182  irredn0  17979  isnzr2  18535  hausnei2  20417  cnhaus  20418  dishaus  20446  ordthauslem  20447  txuni2  20628  xkoopn  20652  txopn  20665  txdis  20695  txdis1cn  20698  pthaus  20701  txhaus  20710  tx1stc  20713  xkohaus  20716  regr1lem  20802  qustgplem  21183  methaus  21583  met2ndci  21585  metnrmlem3  21926  metnrmlem3OLD  21941  elplyr  23203  aaliou2b  23345  aaliou3lem9  23354  2sqlem2  24340  2sqlem8  24348  2sqlem11  24351  2sqb  24354  pntibnd  24479  legov  24678  iscgrad  24901  f1otrge  24950  axsegconlem1  24995  axsegcon  25005  axpaschlem  25018  axlowdimlem6  25025  axlowdim1  25037  axlowdim2  25038  axeuclidlem  25040  el2wlksotot  25658  3cyclfrgrarn1  25788  4cycl2vnunb  25793  br8d  28266  lt2addrd  28374  xlt2addrd  28386  xrnarchi  28549  txomap  28709  tpr2rico  28766  qqhval2  28834  elsx  29064  isanmbfm  29126  br2base  29139  dya2iocnrect  29151  conpcon  30006  br8  30444  br4  30446  fprb  30461  brsegle  30923  hilbert1.1  30969  nn0prpwlem  31026  poimirlem1  31985  itg2addnclem3  32039  cntotbnd  32172  smprngopr  32329  3dim2  33077  llni2  33121  lvoli3  33186  lvoli2  33190  islinei  33349  psubspi2N  33357  elpaddri  33411  eldioph2lem1  35646  diophin  35659  fphpdo  35704  irrapxlem3  35712  irrapxlem4  35713  pellexlem6  35722  pell1234qrreccl  35744  pell1234qrmulcl  35745  pell1234qrdich  35751  pell1qr1  35761  pellqrexplicit  35767  rmxycomplete  35809  dgraalem  36051  dgraalemOLD  36052  fourierdlem64  38071  rspceaov  38736  6gbe  38909  7gbo  38910  8gbe  38911  9gboa  38912  11gboa  38913  structgrssvtxlem  39170  upgredg  39275  upgr4cycl4dv4e  39925  usgvad2edg  39995  modn0mul  40595  elbigo2r  40636