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

Theorem raleqbidv 3145
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1 (𝜑𝐴 = 𝐵)
raleqbidv.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
raleqbidv (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem raleqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
21raleqdv 3137 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43ralbidv 2982 . 2 (𝜑 → (∀𝑥𝐵 𝜓 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 268 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  f12dfv  6494  f13dfv  6495  knatar  6572  ofrfval  6870  fmpt2x  7196  ovmptss  7218  marypha1lem  8299  supeq123d  8316  oieq1  8377  acneq  8826  isfin1a  9074  fpwwe2cbv  9412  fpwwe2lem2  9414  fpwwecbv  9426  fpwwelem  9427  eltskg  9532  elgrug  9574  cau3lem  14044  rlim  14176  ello1  14196  elo1  14207  caurcvg2  14358  caucvgb  14360  fsum2dlem  14448  fsumcom2  14452  fsumcom2OLD  14453  fprod2dlem  14654  fprodcom2  14658  fprodcom2OLD  14659  pcfac  15546  vdwpc  15627  rami  15662  prmgaplem7  15704  prdsval  16055  ismre  16190  isacs2  16254  acsfiel  16255  iscat  16273  iscatd  16274  catidex  16275  catideu  16276  cidfval  16277  cidval  16278  catlid  16284  catrid  16285  comfeq  16306  catpropd  16309  monfval  16332  issubc  16435  fullsubc  16450  isfunc  16464  funcpropd  16500  isfull  16510  isfth  16514  fthpropd  16521  natfval  16546  initoval  16587  termoval  16588  isposd  16895  lubfval  16918  glbfval  16931  ismgm  17183  issstrmgm  17192  grpidval  17200  gsumvalx  17210  gsumpropd  17212  gsumress  17216  issgrp  17225  ismnddef  17236  ismndd  17253  mndpropd  17256  ismhm  17277  resmhm  17299  isgrp  17368  grppropd  17377  isgrpd2e  17381  isnsg  17563  nmznsg  17578  isghm  17600  isga  17664  subgga  17673  gsmsymgrfix  17788  gsmsymgreq  17792  gexval  17933  ispgp  17947  isslw  17963  sylow2blem2  17976  efgval  18070  efgi  18072  efgsdm  18083  cmnpropd  18142  iscmnd  18145  submcmn2  18184  gsumzaddlem  18261  dmdprd  18337  dprdcntz  18347  issrg  18447  isring  18491  ringpropd  18522  isirred  18639  abvfval  18758  abvpropd  18782  islmod  18807  islmodd  18809  lmodprop2d  18865  lssset  18874  islmhm  18967  reslmhm  18992  lmhmpropd  19013  islbs  19016  rrgval  19227  isdomn  19234  isassa  19255  isassad  19263  assapropd  19267  ltbval  19411  opsrval  19414  psgndiflemA  19887  isphl  19913  islindf  20091  islindf2  20093  lsslindf  20109  dmatval  20238  dmatcrng  20248  scmatcrng  20267  cpmat  20454  istopg  20640  restbas  20902  ordtrest2  20948  cnfval  20977  cnpfval  20978  ist0  21064  ishaus  21066  iscnrm  21067  isnrm  21079  ist0-2  21088  ishaus2  21095  nrmsep3  21099  iscmp  21131  is1stc  21184  isptfin  21259  islocfin  21260  kgenval  21278  kgencn2  21300  txbas  21310  ptval  21313  dfac14  21361  isfil  21591  isufil  21647  isufl  21657  flfcntr  21787  ucnval  22021  iscusp  22043  prdsxmslem2  22274  tngngp3  22400  isnlm  22419  nmofval  22458  lebnumii  22705  iscau4  23017  iscmet  23022  iscmet3lem1  23029  iscmet3  23031  equivcmet  23054  ulmcaulem  24086  ulmcau  24087  fsumdvdscom  24845  dchrisumlem3  25114  pntibndlem2  25214  pntibnd  25216  pntlemp  25233  ostth2lem2  25257  trgcgrg  25344  tgcgr4  25360  isismt  25363  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  uvtxaval  26208  uvtxael  26209  uvtxael1  26217  uvtxusgrel  26225  iscplgr  26231  cusgredg  26241  cplgr3v  26252  cplgrop  26254  usgredgsscusgredg  26276  isrgr  26359  isewlk  26402  iswlk  26410  iswwlks  26631  wlkiswwlks2  26664  isclwwlks  26781  clwlkclwwlklem1  26801  isconngr  26949  isconngr1  26950  1conngr  26954  isfrgr  27022  rspc2vd  27029  frgr1v  27033  nfrgr2v  27034  frgr3v  27037  1vwmgr  27038  3vfriswmgr  27040  3cyclfrgrrn1  27047  n4cyclfrgr  27053  frgrncvvdeqlem4  27064  frgrwopreglem4  27076  frgrwopreg2  27080  frgrregorufr0  27081  isplig  27216  gidval  27254  vciOLD  27304  isvclem  27320  isnvlem  27353  lnoval  27495  ajfval  27552  isphg  27560  minvecolem3  27620  htth  27663  ressprs  29482  isslmd  29582  resv1r  29664  iscref  29735  ordtrest2NEW  29793  fmcncfil  29801  issiga  29997  isrnsigaOLD  29998  isrnsiga  29999  isldsys  30042  ismeas  30085  carsgval  30188  issibf  30218  sitgfval  30226  signstfvneq0  30471  istrkg2d  30504  ispconn  30966  issconn  30969  txpconn  30975  cvxpconn  30985  cvmscbv  31001  iscvm  31002  cvmsdisj  31013  cvmsss2  31017  snmlval  31074  elmrsubrn  31178  ismfs  31207  mclsval  31221  fwddifnval  31965  poimirlem28  33108  cover2g  33180  seqpo  33214  incsequz2  33216  caushft  33228  ismtyval  33270  isass  33316  isexid  33317  elghomlem1OLD  33355  isrngo  33367  isrngod  33368  isgrpda  33425  rngohomval  33434  iscom2  33465  idlval  33483  pridlval  33503  maxidlval  33509  lflset  33865  islfld  33868  isopos  33986  isoml  34044  isatl  34105  iscvlat  34129  ishlat1  34158  psubspset  34549  lautset  34887  pautsetN  34903  ldilfset  34913  ltrnfset  34922  dilfsetN  34958  trnfsetN  34961  trnsetN  34962  trlfset  34966  tendofset  35565  tendoset  35566  dihffval  36038  lpolsetN  36290  hdmapfval  36638  hgmapfval  36697  aomclem8  37150  islnm  37166  sdrgacs  37291  clsk1independent  37865  gneispace2  37951  gneispaceel2  37963  gneispacess2  37965  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  issal  39871  isome  40045  iccpartiltu  40686  iccelpart  40697  isupwlk  41035  mgmpropd  41093  ismgmd  41094  ismgmhm  41101  resmgmhm  41116  iscllaw  41143  iscomlaw  41144  isasslaw  41146  isrng  41194  c0snmgmhm  41232  zlidlring  41246  uzlidlring  41247  dmatALTval  41507  islininds  41553  lindslinindsimp2  41570  ldepsnlinc  41615  elbigo  41667
  Copyright terms: Public domain W3C validator