Theorem rspc2ev 3102

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 3094	. . . 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 1183	. 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 2757	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3094	. 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 965   = wceq 1369   e. wcel 1756   E.wrex 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-v 2995

This theorem is referenced by:  rspc3ev  3104  opelxp  4890  rspceov  6149  erov  7218  ralxpmap  7283  2dom  7403  elfiun  7701  dffi3  7702  ixpiunwdom  7827  1re  9406  ello12r  13016  ello1d  13022  elo12r  13027  o1lo1  13036  addcn2  13092  mulcn2  13094  bezoutlem3  13745  bezout  13747  pythagtriplem18  13920  pczpre  13935  pcdiv  13940  4sqlem3  14032  4sqlem4  14034  4sqlem12  14038  vdwlem1  14063  vdwlem6  14068  vdwlem8  14070  vdwlem12  14074  vdwlem13  14075  0ram  14102  ramz2  14106  pmtr3ncom  16002  psgnunilem1  16020  irredn0  16817  isnzr2  17367  hausnei2  18979  cnhaus  18980  dishaus  19008  ordthauslem  19009  txuni2  19160  xkoopn  19184  txopn  19197  txdis  19227  txdis1cn  19230  pthaus  19233  txhaus  19242  tx1stc  19245  xkohaus  19248  regr1lem  19334  divstgplem  19713  methaus  20117  met2ndci  20119  metnrmlem3  20459  elplyr  21691  aaliou2b  21829  aaliou3lem9  21838  2sqlem2  22725  2sqlem8  22733  2sqlem11  22736  2sqb  22739  pntibnd  22864  legov  23038  f1otrge  23140  axsegconlem1  23185  axsegcon  23195  axpaschlem  23208  axlowdimlem6  23215  axlowdim1  23227  axlowdim2  23228  axeuclidlem  23230  br8d  25964  lt2addrd  26058  xlt2addrd  26073  xrnarchi  26223  pstmfval  26345  tpr2rico  26364  qqhval2  26433  elsx  26630  isanmbfm  26693  br2base  26706  dya2iocnrect  26718  conpcon  27146  br8  27588  br4  27590  fprb  27606  brsegle  28161  hilbert1.1  28207  itg2addnclem3  28471  nn0prpwlem  28543  cntotbnd  28721  smprngopr  28878  eldioph2lem1  29124  diophin  29137  fphpdo  29182  irrapxlem3  29191  irrapxlem4  29192  pellexlem6  29201  pell1234qrreccl  29221  pell1234qrmulcl  29222  pell1234qrdich  29228  pell1qr1  29238  pellqrexplicit  29244  rmxycomplete  29284  dgraalem  29528  rspceaov  30129  el2wlksotot  30427  3cyclfrgrarn1  30630  4cycl2vnunb  30635  3dim2  33208  llni2  33252  lvoli3  33317  lvoli2  33321  islinei  33480  psubspi2N  33488  elpaddri  33542