Theorem rspc2ev 3020

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 3012	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 553	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1149	. 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 2687	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3012	. 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 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  rspc3ev  3022  opelxp  4867  rspceov  6075  erov  6960  2dom  7138  elfiun  7393  dffi3  7394  ixpiunwdom  7515  1re  9046  ello12r  12266  ello1d  12272  elo12r  12277  o1lo1  12286  addcn2  12342  mulcn2  12344  bezoutlem3  12995  bezout  12997  pythagtriplem18  13161  pczpre  13176  pcdiv  13181  4sqlem3  13273  4sqlem4  13275  4sqlem12  13279  vdwlem1  13304  vdwlem6  13309  vdwlem8  13311  vdwlem12  13315  vdwlem13  13316  0ram  13343  ramz2  13347  irredn0  15763  isnzr2  16289  hausnei2  17371  cnhaus  17372  dishaus  17400  ordthauslem  17401  txuni2  17550  xkoopn  17574  txopn  17587  txdis  17617  txdis1cn  17620  pthaus  17623  txhaus  17632  tx1stc  17635  xkohaus  17638  regr1lem  17724  divstgplem  18103  methaus  18503  met2ndci  18505  metnrmlem3  18844  elplyr  20073  aaliou2b  20211  aaliou3lem9  20220  2sqlem2  21101  2sqlem8  21109  2sqlem11  21112  2sqb  21115  pntibnd  21240  lt2addrd  24068  xlt2addrd  24077  xrnarchi  24207  pstmfval  24244  tpr2rico  24263  qqhval2  24319  elsx  24501  isanmbfm  24559  br2base  24572  dya2iocnrect  24584  conpcon  24875  br8  25327  br4  25329  fprb  25343  axsegconlem1  25760  axsegcon  25770  axpaschlem  25783  axlowdimlem6  25790  axlowdim1  25802  axlowdim2  25803  axeuclidlem  25805  brsegle  25946  hilbert1.1  25992  itg2addnclem3  26157  nn0prpwlem  26215  cntotbnd  26395  smprngopr  26552  ralxpmap  26632  eldioph2lem1  26708  diophin  26721  fphpdo  26768  irrapxlem3  26777  irrapxlem4  26778  pellexlem6  26787  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell1234qrdich  26814  pell1qr1  26824  pellqrexplicit  26830  rmxycomplete  26870  dgraalem  27218  psgnunilem1  27284  rspceaov  27928  el2wlksotot  28079  3cyclfrgrarn1  28116  4cycl2vnunb  28121  3dim2  29950  llni2  29994  lvoli3  30059  lvoli2  30063  islinei  30222  psubspi2N  30230  elpaddri  30284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918