MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc2ev Unicode version

Theorem rspc2ev 2892
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
StepHypRef Expression
1 rspc2v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
21rspcev 2884 . . . 4  |-  ( ( B  e.  D  /\  ps )  ->  E. y  e.  D  ch )
32anim2i 552 . . 3  |-  ( ( A  e.  C  /\  ( B  e.  D  /\  ps ) )  -> 
( A  e.  C  /\  E. y  e.  D  ch ) )
433impb 1147 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  ( A  e.  C  /\  E. y  e.  D  ch ) )
5 rspc2v.1 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
65rexbidv 2564 . . 3  |-  ( x  =  A  ->  ( E. y  e.  D  ph  <->  E. y  e.  D  ch ) )
76rspcev 2884 . 2  |-  ( ( A  e.  C  /\  E. y  e.  D  ch )  ->  E. x  e.  C  E. y  e.  D  ph )
84, 7syl 15 1  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  E. x  e.  C  E. y  e.  D  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rspc3ev  2894  opelxp  4719  rspceov  5893  erov  6755  2dom  6933  elfiun  7183  dffi3  7184  ixpiunwdom  7305  1re  8837  ello12r  11991  ello1d  11997  elo12r  12002  o1lo1  12011  addcn2  12067  mulcn2  12069  bezoutlem3  12719  bezout  12721  pythagtriplem18  12885  pczpre  12900  pcdiv  12905  4sqlem3  12997  4sqlem4  12999  4sqlem12  13003  vdwlem1  13028  vdwlem6  13033  vdwlem8  13035  vdwlem12  13039  vdwlem13  13040  0ram  13067  ramz2  13071  irredn0  15485  isnzr2  16015  hausnei2  17081  cnhaus  17082  dishaus  17110  ordthauslem  17111  txuni2  17260  xkoopn  17284  txopn  17297  txdis  17326  txdis1cn  17329  pthaus  17332  txhaus  17341  tx1stc  17344  xkohaus  17347  regr1lem  17430  divstgplem  17803  methaus  18066  met2ndci  18068  metnrmlem3  18365  elplyr  19583  aaliou2b  19721  aaliou3lem9  19730  2sqlem2  20603  2sqlem8  20611  2sqlem11  20614  2sqb  20617  pntibnd  20742  ofrn2  23207  lt2addrd  23249  xlt2addrd  23253  tpr2rico  23296  elsx  23525  isanmbfm  23561  br2base  23574  conpcon  23766  br8  24113  br4  24115  fprb  24129  axsegconlem1  24545  axsegcon  24555  axpaschlem  24568  axlowdimlem6  24575  axlowdim1  24587  axlowdim2  24588  axeuclidlem  24590  brsegle  24731  hilbert1.1  24777  rspc2edv  24963  repcpwti  25161  altretop  25600  nn0prpwlem  26238  cntotbnd  26520  smprngopr  26677  ralxpmap  26761  eldioph2lem1  26839  diophin  26852  fphpdo  26900  irrapxlem3  26909  irrapxlem4  26910  pellexlem6  26919  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell1234qrdich  26946  pell1qr1  26956  pellqrexplicit  26962  rmxycomplete  27002  dgraalem  27350  psgnunilem1  27416  rspceaov  28057  3dim2  29657  llni2  29701  lvoli3  29766  lvoli2  29770  islinei  29929  psubspi2N  29937  elpaddri  29991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790
  Copyright terms: Public domain W3C validator