Theorem raleqbidv 3129

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

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	raleqdv 3121	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2969	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 267	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  f12dfv  6429  f13dfv  6430  knatar  6507  ofrfval  6803  fmpt2x  7125  ovmptss  7145  marypha1lem  8222  supeq123d  8239  oieq1  8300  acneq  8749  isfin1a  8997  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwecbv  9345  fpwwelem  9346  eltskg  9451  elgrug  9493  cau3lem  13942  rlim  14074  ello1  14094  elo1  14105  caurcvg2  14256  caucvgb  14258  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  pcfac  15441  vdwpc  15522  rami  15557  prmgaplem7  15599  prdsval  15938  ismre  16073  isacs2  16137  acsfiel  16138  iscat  16156  iscatd  16157  catidex  16158  catideu  16159  cidfval  16160  cidval  16161  catlid  16167  catrid  16168  comfeq  16189  catpropd  16192  monfval  16215  issubc  16318  fullsubc  16333  isfunc  16347  funcpropd  16383  isfull  16393  isfth  16397  fthpropd  16404  natfval  16429  initoval  16470  termoval  16471  isposd  16778  lubfval  16801  glbfval  16814  ismgm  17066  issstrmgm  17075  grpidval  17083  gsumvalx  17093  gsumpropd  17095  gsumress  17099  issgrp  17108  ismnddef  17119  ismndd  17136  mndpropd  17139  ismhm  17160  resmhm  17182  isgrp  17251  grppropd  17260  isgrpd2e  17264  isnsg  17446  nmznsg  17461  isghm  17483  isga  17547  subgga  17556  gsmsymgrfix  17671  gsmsymgreq  17675  gexval  17816  ispgp  17830  isslw  17846  sylow2blem2  17859  efgval  17953  efgi  17955  efgsdm  17966  cmnpropd  18025  iscmnd  18028  submcmn2  18067  gsumzaddlem  18144  dmdprd  18220  dprdcntz  18230  issrg  18330  isring  18374  ringpropd  18405  isirred  18522  abvfval  18641  abvpropd  18665  islmod  18690  islmodd  18692  lmodprop2d  18748  lssset  18755  islmhm  18848  reslmhm  18873  lmhmpropd  18894  islbs  18897  rrgval  19108  isdomn  19115  isassa  19136  isassad  19144  assapropd  19148  ltbval  19292  opsrval  19295  psgndiflemA  19766  isphl  19792  islindf  19970  islindf2  19972  lsslindf  19988  dmatval  20117  dmatcrng  20127  scmatcrng  20146  cpmat  20333  istopg  20525  restbas  20772  ordtrest2  20818  cnfval  20847  cnpfval  20848  ist0  20934  ishaus  20936  iscnrm  20937  isnrm  20949  ist0-2  20958  ishaus2  20965  nrmsep3  20969  iscmp  21001  is1stc  21054  isptfin  21129  islocfin  21130  kgenval  21148  kgencn2  21170  txbas  21180  ptval  21183  dfac14  21231  isfil  21461  isufil  21517  isufl  21527  flfcntr  21657  ucnval  21891  iscusp  21913  prdsxmslem2  22144  tngngp3  22270  isnlm  22289  nmofval  22328  lebnumii  22573  iscau4  22885  iscmet  22890  iscmet3lem1  22897  iscmet3  22899  equivcmet  22922  ulmcaulem  23952  ulmcau  23953  fsumdvdscom  24711  dchrisumlem3  24980  pntibndlem2  25080  pntibnd  25082  pntlemp  25099  ostth2lem2  25123  trgcgrg  25210  tgcgr4  25226  isismt  25229  iscusgra  25985  cusgrarn  25988  cusgra1v  25990  cusgra2v  25991  cusgra3v  25993  usgrasscusgra  26011  isuvtx  26016  uvtxel  26017  cusgrauvtxb  26024  iswlk  26048  wlkelwrd  26058  istrl  26067  constr3trllem2  26179  isconngra  26200  isconngra1  26201  iswwlk  26211  wlkiswwlk2  26225  isclwwlk  26296  clwwlkprop  26298  clwlkisclwwlklem2  26314  isrgra  26453  isfrgra  26517  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3v  26529  1vwmgra  26530  3vfriswmgra  26532  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgrancvvdeqlem4  26560  frgrawopreglem4  26574  frgrawopreg2  26578  frgraregorufr0  26579  isplig  26720  gidval  26750  vciOLD  26800  isvclem  26816  isnvlem  26849  lnoval  26991  ajfval  27048  isphg  27056  minvecolem3  27116  htth  27159  ressprs  28986  isslmd  29086  resv1r  29168  iscref  29239  ordtrest2NEW  29297  fmcncfil  29305  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503  isldsys  29546  ismeas  29589  carsgval  29692  issibf  29722  sitgfval  29730  signstfvneq0  29975  istrkg2d  29997  ispcon  30459  isscon  30462  txpcon  30468  cvxpcon  30478  cvmscbv  30494  iscvm  30495  cvmsdisj  30506  cvmsss2  30510  snmlval  30567  elmrsubrn  30671  ismfs  30700  mclsval  30714  fwddifnval  31440  poimirlem28  32607  cover2g  32679  seqpo  32713  incsequz2  32715  caushft  32727  ismtyval  32769  isass  32815  isexid  32816  elghomlem1OLD  32854  isrngo  32866  isrngod  32867  isgrpda  32924  rngohomval  32933  iscom2  32964  idlval  32982  pridlval  33002  maxidlval  33008  lflset  33364  islfld  33367  isopos  33485  isoml  33543  isatl  33604  iscvlat  33628  ishlat1  33657  psubspset  34048  lautset  34386  pautsetN  34402  ldilfset  34412  ltrnfset  34421  dilfsetN  34457  trnfsetN  34460  trnsetN  34461  trlfset  34465  tendofset  35064  tendoset  35065  dihffval  35537  lpolsetN  35789  hdmapfval  36137  hgmapfval  36196  aomclem8  36649  islnm  36665  sdrgacs  36790  clsk1independent  37364  gneispace2  37450  gneispaceel2  37462  gneispacess2  37464  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  iccpartiltu  39960  iccelpart  39971  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  uvtxaval  40613  uvtxael  40614  uvtxael1  40622  uvtxusgrel  40630  iscplgr  40636  cusgredg  40646  cplgr3v  40657  cplgrop  40659  usgredgsscusgredg  40675  isrgr  40759  isewlk  40804  is1wlk  40813  isWlk  40814  iswwlks  41039  1wlkiswwlks2  41072  isclwwlks  41188  clwlkclwwlklem1  41208  isconngr  41356  isconngr1  41357  1conngr  41361  isfrgr  41430  rspc2vd  41437  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  1vwmgr  41446  3vfriswmgr  41448  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrncvvdeqlem4  41472  frgrwopreglem4  41484  frgrwopreg2  41488  frgrregorufr0  41489  mgmpropd  41565  ismgmd  41566  ismgmhm  41573  resmgmhm  41588  iscllaw  41615  iscomlaw  41616  isasslaw  41618  isrng  41666  c0snmgmhm  41704  zlidlring  41718  uzlidlring  41719  dmatALTval  41983  islininds  42029  lindslinindsimp2  42046  ldepsnlinc  42091  elbigo  42143