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

Theorem raleqbidv 3072
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1  |-  ( ph  ->  A  =  B )
raleqbidv.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
raleqbidv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem raleqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
21raleqdv 3064 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2903 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 253 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   A.wral 2814
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-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  f12dfv  6167  f13dfv  6168  knatar  6241  ofrfval  6532  fmpt2x  6850  ovmptss  6864  marypha1lem  7893  supeq123d  7910  oieq1  7937  acneq  8424  isfin1a  8672  fpwwe2cbv  9008  fpwwe2lem2  9010  fpwwecbv  9022  fpwwelem  9023  eltskg  9128  elgrug  9170  cau3lem  13150  rlim  13281  ello1  13301  elo1  13312  caurcvg2  13463  caucvgb  13465  fsum2dlem  13548  fsumcom2  13552  pcfac  14277  vdwpc  14357  rami  14392  prdsval  14710  ismre  14845  isacs2  14908  acsfiel  14909  iscat  14927  iscatd  14928  catidex  14929  catideu  14930  cidfval  14931  cidval  14932  catlid  14938  catrid  14939  comfeq  14962  catpropd  14965  monfval  14988  issubc  15065  fullsubc  15077  isfunc  15091  funcpropd  15127  isfull  15137  isfth  15141  fthpropd  15148  natfval  15173  isposd  15442  lubfval  15465  glbfval  15478  ismnd  15734  grpidval  15749  ismndd  15761  mndpropd  15764  ismhm  15788  resmhm  15809  gsumvalx  15824  gsumpropd  15826  gsumress  15829  isgrp  15871  grppropd  15878  isgrpd2e  15882  isnsg  16035  nmznsg  16050  isghm  16072  isga  16134  subgga  16143  gsmsymgrfix  16258  gsmsymgreq  16262  gexval  16404  ispgp  16418  isslw  16434  sylow2blem2  16447  efgval  16541  efgi  16543  efgsdm  16554  cmnpropd  16613  iscmnd  16616  submcmn2  16650  gsumzaddlem  16737  gsumzaddlemOLD  16739  dmdprd  16832  dprdcntz  16844  issrg  16961  isrng  17004  rngpropd  17031  isirred  17149  abvfval  17267  abvpropd  17291  islmod  17316  islmodd  17318  lmodprop2d  17372  lssset  17380  islmhm  17473  reslmhm  17498  lmhmpropd  17519  islbs  17522  rrgval  17734  isdomn  17742  isassa  17763  isassad  17771  assapropd  17775  ltbval  17935  opsrval  17938  psgndiflemA  18432  isphl  18458  islindf  18642  islindf2  18644  lsslindf  18660  dmatval  18789  dmatcrng  18799  scmatcrng  18818  cpmat  19005  istopg  19199  restbas  19453  ordtrest2  19499  cnfval  19528  cnpfval  19529  ist0  19615  ishaus  19617  iscnrm  19618  isnrm  19630  ist0-2  19639  ishaus2  19646  nrmsep3  19650  iscmp  19682  is1stc  19736  kgenval  19799  kgencn2  19821  txbas  19831  ptval  19834  dfac14  19882  isfil  20111  isufil  20167  isufl  20177  ucnval  20543  iscusp  20565  prdsxmslem2  20795  isnlm  20947  nmofval  20984  lebnumii  21229  iscau4  21481  iscmet  21486  iscmet3lem1  21493  iscmet3  21495  equivcmet  21517  ulmcaulem  22551  ulmcau  22552  fsumdvdscom  23217  dchrisumlem3  23432  pntibndlem2  23532  pntibnd  23534  pntlemp  23551  ostth2lem2  23575  istrkg2d  23612  trgcgrg  23662  isismt  23677  iscusgra  24160  cusgrarn  24163  cusgra1v  24165  cusgra2v  24166  cusgra3v  24168  usgrasscusgra  24187  isuvtx  24192  uvtxel  24193  cusgrauvtxb  24200  iswlk  24224  wlkelwrd  24234  istrl  24243  constr3trllem2  24355  isconngra  24376  isconngra1  24377  iswwlk  24387  wlkiswwlk2  24401  wwlkn0s  24409  isclwwlk  24472  clwwlkprop  24474  clwlkisclwwlklem2  24490  isrgra  24630  isrgrac  24638  isfrgra  24694  frgraunss  24699  frgra1v  24702  frgra2v  24703  frgra3v  24706  1vwmgra  24707  3vfriswmgra  24709  3cyclfrgrarn1  24716  n4cyclfrgra  24722  frgrancvvdeqlem4  24738  frgrawopreglem4  24752  frgrawopreg2  24756  frgraregorufr0  24757  isplig  24883  gidval  24919  isgrp2d  24941  isgrpda  25003  isass  25022  isexid  25023  elghomlem1  25067  isrngo  25084  isrngod  25085  iscom2  25118  vci  25145  isvclem  25174  isnvlem  25207  lnoval  25371  ajfval  25428  isphg  25436  minvecolem3  25496  htth  25539  ressprs  27333  isslmd  27435  resv1r  27518  ordtrest2NEW  27569  fmcncfil  27577  issiga  27779  isrnsigaOLD  27780  isrnsiga  27781  ismeas  27838  issibf  27943  sitgfval  27951  signstfvneq0  28197  ispcon  28336  isscon  28339  txpcon  28345  cvxpcon  28355  cvmscbv  28371  iscvm  28372  cvmsdisj  28383  cvmsss2  28387  snmlval  28444  fprod2dlem  28715  fprodcom2  28719  isptfin  29795  islocfin  29796  cover2g  29836  seqpo  29871  incsequz2  29873  caushft  29885  ismtyval  29927  rngohomval  29998  idlval  30041  pridlval  30061  maxidlval  30067  aomclem8  30639  islnm  30655  sdrgacs  30783  ismgmALT  31951  issgrp  31954  sgrpplusgaop  31962  iscllaw  31969  iscomlaw  31970  isasslaw  31972  isrng0  32013  dmatALTval  32100  islininds  32146  lindslinindsimp2  32163  ldepsnlinc  32208  lflset  33874  islfld  33877  isopos  33995  isoml  34053  isatl  34114  iscvlat  34138  ishlat1  34167  psubspset  34558  lautset  34896  pautsetN  34912  ldilfset  34922  ltrnfset  34931  dilfsetN  34966  trnfsetN  34969  trnsetN  34970  trlfset  34974  tendofset  35572  tendoset  35573  dihffval  36045  lpolsetN  36297  hdmapfval  36645  hgmapfval  36704
  Copyright terms: Public domain W3C validator