Theorem rspc2ev 3194

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 3183	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 572	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1202	. 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 2940	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3183	. 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 188   /\ wa 371   /\ w3a 983   = wceq 1438   e. wcel 1869   E.wrex 2777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-v 3084

This theorem is referenced by:  rspc3ev  3196  opelxp  4881  f1prex  6195  rspceov  6342  erov  7466  ralxpmap  7527  2dom  7647  elfiun  7948  dffi3  7949  ixpiunwdom  8110  1re  9644  ello12r  13574  ello1d  13580  elo12r  13585  o1lo1  13594  addcn2  13650  mulcn2  13652  bezoutlem3OLD  14498  bezoutlem3  14501  bezout  14503  pythagtriplem18  14775  pczpre  14790  pcdiv  14795  4sqlem3  14887  4sqlem4  14889  4sqlem12  14893  vdwlem1  14924  vdwlem6  14929  vdwlem8  14931  vdwlem12  14935  vdwlem13  14936  0ram  14971  ramz2  14975  sgrp2rid2ex  16654  pmtr3ncom  17109  psgnunilem1  17127  irredn0  17924  isnzr2  18480  hausnei2  20361  cnhaus  20362  dishaus  20390  ordthauslem  20391  txuni2  20572  xkoopn  20596  txopn  20609  txdis  20639  txdis1cn  20642  pthaus  20645  txhaus  20654  tx1stc  20657  xkohaus  20660  regr1lem  20746  qustgplem  21127  methaus  21527  met2ndci  21529  metnrmlem3  21870  metnrmlem3OLD  21885  elplyr  23147  aaliou2b  23289  aaliou3lem9  23298  2sqlem2  24284  2sqlem8  24292  2sqlem11  24295  2sqb  24298  pntibnd  24423  legov  24622  iscgrad  24845  f1otrge  24894  axsegconlem1  24939  axsegcon  24949  axpaschlem  24962  axlowdimlem6  24969  axlowdim1  24981  axlowdim2  24982  axeuclidlem  24984  el2wlksotot  25602  3cyclfrgrarn1  25732  4cycl2vnunb  25737  br8d  28214  lt2addrd  28326  xlt2addrd  28338  xrnarchi  28502  txomap  28663  tpr2rico  28720  qqhval2  28788  elsx  29018  isanmbfm  29080  br2base  29093  dya2iocnrect  29105  conpcon  29960  br8  30397  br4  30399  fprb  30414  brsegle  30874  hilbert1.1  30920  nn0prpwlem  30977  poimirlem1  31861  itg2addnclem3  31915  cntotbnd  32048  smprngopr  32205  3dim2  32958  llni2  33002  lvoli3  33067  lvoli2  33071  islinei  33230  psubspi2N  33238  elpaddri  33292  eldioph2lem1  35527  diophin  35540  fphpdo  35585  irrapxlem3  35594  irrapxlem4  35595  pellexlem6  35604  pell1234qrreccl  35626  pell1234qrmulcl  35627  pell1234qrdich  35633  pell1qr1  35643  pellqrexplicit  35649  rmxycomplete  35691  dgraalem  35933  dgraalemOLD  35934  fourierdlem64  37860  rspceaov  38417  6gbe  38590  7gbo  38591  8gbe  38592  9gboa  38593  11gboa  38594  struct1vtxvallem  38795  usgvad2edg  39027  modn0mul  39629  elbigo2r  39670