Theorem rspc2ev 3225

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 3214	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 569	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1192	. 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 2973	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3214	. 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 973   = wceq 1379   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-v 3115

This theorem is referenced by:  rspc3ev  3227  opelxp  5029  rspceov  6321  erov  7408  ralxpmap  7468  2dom  7588  elfiun  7890  dffi3  7891  ixpiunwdom  8017  1re  9595  ello12r  13303  ello1d  13309  elo12r  13314  o1lo1  13323  addcn2  13379  mulcn2  13381  bezoutlem3  14037  bezout  14039  pythagtriplem18  14215  pczpre  14230  pcdiv  14235  4sqlem3  14327  4sqlem4  14329  4sqlem12  14333  vdwlem1  14358  vdwlem6  14363  vdwlem8  14365  vdwlem12  14369  vdwlem13  14370  0ram  14397  ramz2  14401  pmtr3ncom  16306  psgnunilem1  16324  irredn0  17153  isnzr2  17710  hausnei2  19648  cnhaus  19649  dishaus  19677  ordthauslem  19678  txuni2  19829  xkoopn  19853  txopn  19866  txdis  19896  txdis1cn  19899  pthaus  19902  txhaus  19911  tx1stc  19914  xkohaus  19917  regr1lem  20003  divstgplem  20382  methaus  20786  met2ndci  20788  metnrmlem3  21128  elplyr  22361  aaliou2b  22499  aaliou3lem9  22508  2sqlem2  23395  2sqlem8  23403  2sqlem11  23406  2sqb  23409  pntibnd  23534  legov  23727  f1otrge  23879  axsegconlem1  23924  axsegcon  23934  axpaschlem  23947  axlowdimlem6  23954  axlowdim1  23966  axlowdim2  23967  axeuclidlem  23969  el2wlksotot  24586  3cyclfrgrarn1  24716  4cycl2vnunb  24721  br8d  27164  lt2addrd  27259  xlt2addrd  27274  xrnarchi  27418  txomap  27528  pstmfval  27539  tpr2rico  27558  qqhval2  27627  elsx  27833  isanmbfm  27895  br2base  27908  dya2iocnrect  27920  conpcon  28348  br8  28790  br4  28792  fprb  28808  brsegle  29363  hilbert1.1  29409  itg2addnclem3  29673  nn0prpwlem  29745  cntotbnd  29923  smprngopr  30080  eldioph2lem1  30325  diophin  30338  fphpdo  30383  irrapxlem3  30392  irrapxlem4  30393  pellexlem6  30402  pell1234qrreccl  30422  pell1234qrmulcl  30423  pell1234qrdich  30429  pell1qr1  30439  pellqrexplicit  30445  rmxycomplete  30485  dgraalem  30727  fourierdlem64  31499  rspceaov  31777  usgvad2edg  31906  3dim2  34282  llni2  34326  lvoli3  34391  lvoli2  34395  islinei  34554  psubspi2N  34562  elpaddri  34616