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

Theorem raleqbidv 3182
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 3174 . 2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43ralbidv 3015 . 2 (𝜑 → (∀𝑥𝐵 𝜓 ↔ ∀𝑥𝐵 𝜒))
52, 4bitrd 268 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  f12dfv  6569  f13dfv  6570  knatar  6647  ofrfval  6947  fmpt2x  7281  ovmptss  7303  marypha1lem  8380  supeq123d  8397  oieq1  8458  acneq  8904  isfin1a  9152  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwecbv  9504  fpwwelem  9505  eltskg  9610  elgrug  9652  cau3lem  14138  rlim  14270  ello1  14290  elo1  14301  caurcvg2  14452  caucvgb  14454  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  pcfac  15650  vdwpc  15731  rami  15766  prmgaplem7  15808  prdsval  16162  ismre  16297  isacs2  16361  acsfiel  16362  iscat  16380  iscatd  16381  catidex  16382  catideu  16383  cidfval  16384  cidval  16385  catlid  16391  catrid  16392  comfeq  16413  catpropd  16416  monfval  16439  issubc  16542  fullsubc  16557  isfunc  16571  funcpropd  16607  isfull  16617  isfth  16621  fthpropd  16628  natfval  16653  initoval  16694  termoval  16695  isposd  17002  lubfval  17025  glbfval  17038  ismgm  17290  issstrmgm  17299  grpidval  17307  gsumvalx  17317  gsumpropd  17319  gsumress  17323  issgrp  17332  ismnddef  17343  ismndd  17360  mndpropd  17363  ismhm  17384  resmhm  17406  isgrp  17475  grppropd  17484  isgrpd2e  17488  isnsg  17670  nmznsg  17685  isghm  17707  isga  17770  subgga  17779  gsmsymgrfix  17894  gsmsymgreq  17898  gexval  18039  ispgp  18053  isslw  18069  sylow2blem2  18082  efgval  18176  efgi  18178  efgsdm  18189  cmnpropd  18248  iscmnd  18251  submcmn2  18290  gsumzaddlem  18367  dmdprd  18443  dprdcntz  18453  issrg  18553  isring  18597  ringpropd  18628  isirred  18745  abvfval  18866  abvpropd  18890  islmod  18915  islmodd  18917  lmodprop2d  18973  lssset  18982  islmhm  19075  reslmhm  19100  lmhmpropd  19121  islbs  19124  rrgval  19335  isdomn  19342  isassa  19363  isassad  19371  assapropd  19375  ltbval  19519  opsrval  19522  psgndiflemA  19995  isphl  20021  islindf  20199  islindf2  20201  lsslindf  20217  dmatval  20346  dmatcrng  20356  scmatcrng  20375  cpmat  20562  istopg  20748  restbas  21010  ordtrest2  21056  cnfval  21085  cnpfval  21086  ist0  21172  ishaus  21174  iscnrm  21175  isnrm  21187  ist0-2  21196  ishaus2  21203  nrmsep3  21207  iscmp  21239  is1stc  21292  isptfin  21367  islocfin  21368  kgenval  21386  kgencn2  21408  txbas  21418  ptval  21421  dfac14  21469  isfil  21698  isufil  21754  isufl  21764  flfcntr  21894  ucnval  22128  iscusp  22150  prdsxmslem2  22381  tngngp3  22507  isnlm  22526  nmofval  22565  lebnumii  22812  iscau4  23123  iscmet  23128  iscmet3lem1  23135  iscmet3  23137  equivcmet  23160  ulmcaulem  24193  ulmcau  24194  fsumdvdscom  24956  dchrisumlem3  25225  pntibndlem2  25325  pntibnd  25327  pntlemp  25344  ostth2lem2  25368  trgcgrg  25455  tgcgr4  25471  isismt  25474  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  uvtxval  26333  uvtxavalOLD  26334  uvtxel  26335  uvtxaelOLD  26336  uvtxel1  26345  uvtxael1OLD  26347  uvtxusgrel  26354  cusgredg  26376  cplgr3v  26387  cplgrop  26389  usgredgsscusgredg  26411  isrgr  26511  isewlk  26554  iswlk  26562  iswwlks  26784  wlkiswwlks2  26829  isclwwlk  26952  clwlkclwwlklem1  26965  isconngr  27167  isconngr1  27168  1conngr  27172  isfrgr  27238  rspc2vd  27245  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  1vwmgr  27256  3vfriswmgr  27258  3cyclfrgrrn1  27265  n4cyclfrgr  27271  isplig  27458  gidval  27494  vciOLD  27544  isvclem  27560  isnvlem  27593  lnoval  27735  ajfval  27792  isphg  27800  minvecolem3  27860  htth  27903  ressprs  29783  isslmd  29883  resv1r  29965  iscref  30039  ordtrest2NEW  30097  fmcncfil  30105  issiga  30302  isrnsigaOLD  30303  isrnsiga  30304  isldsys  30347  ismeas  30390  carsgval  30493  issibf  30523  sitgfval  30531  signstfvneq0  30777  istrkg2d  30872  ispconn  31331  issconn  31334  txpconn  31340  cvxpconn  31350  cvmscbv  31366  iscvm  31367  cvmsdisj  31378  cvmsss2  31382  snmlval  31439  elmrsubrn  31543  ismfs  31572  mclsval  31586  frrlem4  31908  fwddifnval  32395  bj-ismoore  33184  poimirlem28  33567  cover2g  33639  seqpo  33673  incsequz2  33675  caushft  33687  ismtyval  33729  isass  33775  isexid  33776  elghomlem1OLD  33814  isrngo  33826  isrngod  33827  isgrpda  33884  rngohomval  33893  iscom2  33924  idlval  33942  pridlval  33962  maxidlval  33968  elrefrels3  34408  elcnvrefrels3  34421  lflset  34664  islfld  34667  isopos  34785  isoml  34843  isatl  34904  iscvlat  34928  ishlat1  34957  psubspset  35348  lautset  35686  pautsetN  35702  ldilfset  35712  ltrnfset  35721  dilfsetN  35757  trnfsetN  35760  trnsetN  35761  trlfset  35765  tendofset  36363  tendoset  36364  dihffval  36836  lpolsetN  37088  hdmapfval  37436  hgmapfval  37495  aomclem8  37948  islnm  37964  sdrgacs  38088  clsk1independent  38661  gneispace2  38747  gneispaceel2  38759  gneispacess2  38761  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  issal  40852  isome  41029  iccpartiltu  41683  iccelpart  41694  isupwlk  42042  mgmpropd  42100  ismgmd  42101  ismgmhm  42108  resmgmhm  42123  iscllaw  42150  iscomlaw  42151  isasslaw  42153  isrng  42201  c0snmgmhm  42239  zlidlring  42253  uzlidlring  42254  dmatALTval  42514  islininds  42560  lindslinindsimp2  42577  ldepsnlinc  42622  elbigo  42670
  Copyright terms: Public domain W3C validator