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

Theorem raleqbidv 3128
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 3120 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43ralbidv 2968 . 2 (𝜑 → (∀𝑥𝐵 𝜓 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 266 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900
This theorem is referenced by:  f12dfv  6407  f13dfv  6408  knatar  6485  ofrfval  6780  fmpt2x  7102  ovmptss  7122  marypha1lem  8199  supeq123d  8216  oieq1  8277  acneq  8726  isfin1a  8974  fpwwe2cbv  9308  fpwwe2lem2  9310  fpwwecbv  9322  fpwwelem  9323  eltskg  9428  elgrug  9470  cau3lem  13888  rlim  14020  ello1  14040  elo1  14051  caurcvg2  14202  caucvgb  14204  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  pcfac  15387  vdwpc  15468  rami  15503  prmgaplem7  15545  prdsval  15884  ismre  16019  isacs2  16083  acsfiel  16084  iscat  16102  iscatd  16103  catidex  16104  catideu  16105  cidfval  16106  cidval  16107  catlid  16113  catrid  16114  comfeq  16135  catpropd  16138  monfval  16161  issubc  16264  fullsubc  16279  isfunc  16293  funcpropd  16329  isfull  16339  isfth  16343  fthpropd  16350  natfval  16375  initoval  16416  termoval  16417  isposd  16724  lubfval  16747  glbfval  16760  ismgm  17012  issstrmgm  17021  grpidval  17029  gsumvalx  17039  gsumpropd  17041  gsumress  17045  issgrp  17054  ismnddef  17065  ismndd  17082  mndpropd  17085  ismhm  17106  resmhm  17128  isgrp  17197  grppropd  17206  isgrpd2e  17210  isnsg  17392  nmznsg  17407  isghm  17429  isga  17493  subgga  17502  gsmsymgrfix  17617  gsmsymgreq  17621  gexval  17762  ispgp  17776  isslw  17792  sylow2blem2  17805  efgval  17899  efgi  17901  efgsdm  17912  cmnpropd  17971  iscmnd  17974  submcmn2  18013  gsumzaddlem  18090  dmdprd  18166  dprdcntz  18176  issrg  18276  isring  18320  ringpropd  18351  isirred  18468  abvfval  18587  abvpropd  18611  islmod  18636  islmodd  18638  lmodprop2d  18694  lssset  18701  islmhm  18794  reslmhm  18819  lmhmpropd  18840  islbs  18843  rrgval  19054  isdomn  19061  isassa  19082  isassad  19090  assapropd  19094  ltbval  19238  opsrval  19241  psgndiflemA  19711  isphl  19737  islindf  19912  islindf2  19914  lsslindf  19930  dmatval  20059  dmatcrng  20069  scmatcrng  20088  cpmat  20275  istopg  20467  restbas  20714  ordtrest2  20760  cnfval  20789  cnpfval  20790  ist0  20876  ishaus  20878  iscnrm  20879  isnrm  20891  ist0-2  20900  ishaus2  20907  nrmsep3  20911  iscmp  20943  is1stc  20996  isptfin  21071  islocfin  21072  kgenval  21090  kgencn2  21112  txbas  21122  ptval  21125  dfac14  21173  isfil  21403  isufil  21459  isufl  21469  flfcntr  21599  ucnval  21833  iscusp  21855  prdsxmslem2  22085  isnlm  22222  nmofval  22260  lebnumii  22504  iscau4  22803  iscmet  22808  iscmet3lem1  22815  iscmet3  22817  equivcmet  22839  ulmcaulem  23869  ulmcau  23870  fsumdvdscom  24628  dchrisumlem3  24897  pntibndlem2  24997  pntibnd  24999  pntlemp  25016  ostth2lem2  25040  trgcgrg  25128  tgcgr4  25144  isismt  25147  iscusgra  25751  cusgrarn  25754  cusgra1v  25756  cusgra2v  25757  cusgra3v  25759  usgrasscusgra  25777  isuvtx  25782  uvtxel  25783  cusgrauvtxb  25790  iswlk  25814  wlkelwrd  25824  istrl  25833  constr3trllem2  25945  isconngra  25966  isconngra1  25967  iswwlk  25977  wlkiswwlk2  25991  isclwwlk  26062  clwwlkprop  26064  clwlkisclwwlklem2  26080  isrgra  26219  isfrgra  26283  frgraunss  26288  frgra1v  26291  frgra2v  26292  frgra3v  26295  1vwmgra  26296  3vfriswmgra  26298  3cyclfrgrarn1  26305  n4cyclfrgra  26311  frgrancvvdeqlem4  26326  frgrawopreglem4  26340  frgrawopreg2  26344  frgraregorufr0  26345  isplig  26486  gidval  26516  vciOLD  26569  isvclem  26598  isnvlem  26633  lnoval  26797  ajfval  26854  isphg  26862  minvecolem3  26922  htth  26965  ressprs  28792  isslmd  28892  resv1r  28974  iscref  29045  ordtrest2NEW  29103  fmcncfil  29111  issiga  29307  isrnsigaOLD  29308  isrnsiga  29309  isldsys  29352  ismeas  29395  carsgval  29498  issibf  29528  sitgfval  29536  signstfvneq0  29781  istrkg2d  29803  ispcon  30265  isscon  30268  txpcon  30274  cvxpcon  30284  cvmscbv  30300  iscvm  30301  cvmsdisj  30312  cvmsss2  30316  snmlval  30373  elmrsubrn  30477  ismfs  30506  mclsval  30520  fwddifnval  31246  poimirlem28  32410  cover2g  32482  seqpo  32516  incsequz2  32518  caushft  32530  ismtyval  32572  isass  32618  isexid  32619  elghomlem1OLD  32657  isrngo  32669  isrngod  32670  isgrpda  32727  rngohomval  32736  iscom2  32767  idlval  32785  pridlval  32805  maxidlval  32811  lflset  33167  islfld  33170  isopos  33288  isoml  33346  isatl  33407  iscvlat  33431  ishlat1  33460  psubspset  33851  lautset  34189  pautsetN  34205  ldilfset  34215  ltrnfset  34224  dilfsetN  34260  trnfsetN  34263  trnsetN  34264  trlfset  34268  tendofset  34867  tendoset  34868  dihffval  35340  lpolsetN  35592  hdmapfval  35940  hgmapfval  35999  aomclem8  36452  islnm  36468  sdrgacs  36593  clsk1independent  37167  gneispace2  37253  gneispaceel2  37265  gneispacess2  37267  ioodvbdlimc1lem1  38625  ioodvbdlimc1lem2  38626  ioodvbdlimc2lem  38628  iccpartiltu  39765  iccelpart  39776  nbgr2vtx1edg  40574  nbuhgr2vtx1edgb  40576  uvtxaval  40615  uvtxael  40616  uvtxael1  40624  uvtxusgrel  40632  iscplgr  40638  cusgredg  40648  cplgr3v  40659  cplgrop  40661  usgredgsscusgredg  40677  isrgr  40761  isewlk  40806  is1wlk  40815  isWlk  40816  iswwlks  41041  1wlkiswwlks2  41074  isclwwlks  41190  clwlkclwwlklem1  41210  isconngr  41358  isconngr1  41359  1conngr  41363  isfrgr  41432  rspc2vd  41439  frgr1v  41443  nfrgr2v  41444  frgr3v  41447  1vwmgr  41448  3vfriswmgr  41450  3cyclfrgrrn1  41457  n4cyclfrgr  41463  frgrncvvdeqlem4  41474  frgrwopreglem4  41486  frgrwopreg2  41490  frgrregorufr0  41491  mgmpropd  41567  ismgmd  41568  ismgmhm  41575  resmgmhm  41590  iscllaw  41617  iscomlaw  41618  isasslaw  41620  isrng  41668  c0snmgmhm  41706  zlidlring  41720  uzlidlring  41721  dmatALTval  41985  islininds  42031  lindslinindsimp2  42048  ldepsnlinc  42093  elbigo  42145
  Copyright terms: Public domain W3C validator