Theorem rspc2ev 3218

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 3207	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 567	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1190	. 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 2965	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3207	. 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 367   /\ w3a 971   = wceq 1398   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-v 3108

This theorem is referenced by:  rspc3ev  3220  opelxp  5018  rspceov  6309  erov  7400  ralxpmap  7461  2dom  7581  elfiun  7882  dffi3  7883  ixpiunwdom  8009  1re  9584  ello12r  13422  ello1d  13428  elo12r  13433  o1lo1  13442  addcn2  13498  mulcn2  13500  bezoutlem3  14262  bezout  14264  pythagtriplem18  14440  pczpre  14455  pcdiv  14460  4sqlem3  14552  4sqlem4  14554  4sqlem12  14558  vdwlem1  14583  vdwlem6  14588  vdwlem8  14590  vdwlem12  14594  vdwlem13  14595  0ram  14622  ramz2  14626  sgrp2rid2ex  16244  pmtr3ncom  16699  psgnunilem1  16717  irredn0  17547  isnzr2  18106  hausnei2  20021  cnhaus  20022  dishaus  20050  ordthauslem  20051  txuni2  20232  xkoopn  20256  txopn  20269  txdis  20299  txdis1cn  20302  pthaus  20305  txhaus  20314  tx1stc  20317  xkohaus  20320  regr1lem  20406  qustgplem  20785  methaus  21189  met2ndci  21191  metnrmlem3  21531  elplyr  22764  aaliou2b  22903  aaliou3lem9  22912  2sqlem2  23837  2sqlem8  23845  2sqlem11  23848  2sqb  23851  pntibnd  23976  legov  24173  cgraid  24371  f1otrge  24377  axsegconlem1  24422  axsegcon  24432  axpaschlem  24445  axlowdimlem6  24452  axlowdim1  24464  axlowdim2  24465  axeuclidlem  24467  el2wlksotot  25084  3cyclfrgrarn1  25214  4cycl2vnunb  25219  br8d  27678  lt2addrd  27794  xlt2addrd  27809  xrnarchi  27962  txomap  28072  tpr2rico  28129  qqhval2  28197  elsx  28402  isanmbfm  28464  br2base  28477  dya2iocnrect  28489  conpcon  28944  br8  29426  br4  29428  fprb  29443  brsegle  29986  hilbert1.1  30032  itg2addnclem3  30308  nn0prpwlem  30380  cntotbnd  30532  smprngopr  30689  eldioph2lem1  30932  diophin  30945  fphpdo  30990  irrapxlem3  30999  irrapxlem4  31000  pellexlem6  31009  pell1234qrreccl  31029  pell1234qrmulcl  31030  pell1234qrdich  31036  pell1qr1  31046  pellqrexplicit  31052  rmxycomplete  31092  dgraalem  31335  fourierdlem64  32192  rspceaov  32521  usgvad2edg  32783  modn0mul  33387  elbigo2r  33428  3dim2  35589  llni2  35633  lvoli3  35698  lvoli2  35702  islinei  35861  psubspi2N  35869  elpaddri  35923