Theorem raleqbidv 3341

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 3333	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 3174	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 270	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ∀wral 3096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101

This theorem is referenced by:  f12dfv  6749  f13dfv  6750  knatar  6827  ofrfval  7131  fmpt2x  7465  ovmptss  7488  marypha1lem  8574  supeq123d  8591  oieq1  8652  acneq  9145  isfin1a  9395  fpwwe2cbv  9733  fpwwe2lem2  9735  fpwwecbv  9747  fpwwelem  9748  eltskg  9853  elgrug  9895  cau3lem  14313  rlim  14445  ello1  14465  elo1  14476  caurcvg2  14627  caucvgb  14629  fsum2dlem  14720  fsumcom2  14724  fprod2dlem  14927  fprodcom2  14931  pcfac  15816  vdwpc  15897  rami  15932  prmgaplem7  15974  prdsval  16316  ismre  16451  isacs2  16514  acsfiel  16515  iscat  16533  iscatd  16534  catidex  16535  catideu  16536  cidfval  16537  cidval  16538  catlid  16544  catrid  16545  comfeq  16566  catpropd  16569  monfval  16592  issubc  16695  fullsubc  16710  isfunc  16724  funcpropd  16760  isfull  16770  isfth  16774  fthpropd  16781  natfval  16806  initoval  16847  termoval  16848  isposd  17156  lubfval  17179  glbfval  17192  ismgm  17444  issstrmgm  17453  grpidval  17461  gsumvalx  17471  gsumpropd  17473  gsumress  17477  issgrp  17486  ismnddef  17497  ismndd  17514  mndpropd  17517  ismhm  17538  resmhm  17560  isgrp  17629  grppropd  17638  isgrpd2e  17642  isnsg  17821  nmznsg  17836  isghm  17858  isga  17921  subgga  17930  gsmsymgrfix  18045  gsmsymgreq  18049  gexval  18190  ispgp  18204  isslw  18220  sylow2blem2  18233  efgval  18327  efgi  18329  efgsdm  18340  cmnpropd  18399  iscmnd  18402  submcmn2  18441  gsumzaddlem  18518  dmdprd  18595  dprdcntz  18605  issrg  18705  isring  18749  ringpropd  18780  isirred  18897  abvfval  19018  abvpropd  19042  islmod  19067  islmodd  19069  lmodprop2d  19125  lssset  19134  islmhm  19230  reslmhm  19255  lmhmpropd  19276  islbs  19279  rrgval  19492  isdomn  19499  isassa  19520  isassad  19528  assapropd  19532  ltbval  19676  opsrval  19679  psgndiflemA  20151  isphl  20179  islindf  20357  islindf2  20359  lsslindf  20375  dmatval  20505  dmatcrng  20515  scmatcrng  20534  cpmat  20723  istopg  20909  restbas  21172  ordtrest2  21218  cnfval  21247  cnpfval  21248  ist0  21334  ishaus  21336  iscnrm  21337  isnrm  21349  ist0-2  21358  ishaus2  21365  nrmsep3  21369  iscmp  21401  is1stc  21454  isptfin  21529  islocfin  21530  kgenval  21548  kgencn2  21570  txbas  21580  ptval  21583  dfac14  21631  isfil  21860  isufil  21916  isufl  21926  flfcntr  22056  ucnval  22290  iscusp  22312  prdsxmslem2  22543  tngngp3  22669  isnlm  22688  nmofval  22727  lebnumii  22974  iscau4  23285  iscmet  23290  iscmet3lem1  23297  iscmet3  23299  equivcmet  23322  ulmcaulem  24358  ulmcau  24359  fsumdvdscom  25121  dchrisumlem3  25390  pntibndlem2  25490  pntibnd  25492  pntlemp  25509  ostth2lem2  25533  trgcgrg  25620  tgcgr4  25636  isismt  25639  nbgr2vtx1edg  26458  nbuhgr2vtx1edgb  26460  uvtxval  26501  uvtxavalOLD  26502  uvtxel  26503  uvtxaelOLD  26504  uvtxel1  26513  uvtxael1OLD  26515  uvtxusgrel  26522  cusgredg  26544  cplgr3v  26555  cplgrop  26557  usgredgsscusgredg  26579  isrgr  26679  isewlk  26722  iswlk  26730  iswwlks  26953  wlkiswwlks2  26998  isclwwlk  27123  clwlkclwwlklem1  27138  isconngr  27358  isconngr1  27359  1conngr  27363  isfrgr  27429  rspc2vd  27436  frgr1v  27442  nfrgr2v  27443  frgr3v  27446  1vwmgr  27447  3vfriswmgr  27449  3cyclfrgrrn1  27456  n4cyclfrgr  27462  isplig  27655  gidval  27691  vciOLD  27740  isvclem  27756  isnvlem  27789  lnoval  27931  ajfval  27988  isphg  27996  minvecolem3  28056  htth  28099  ressprs  29976  isslmd  30076  resv1r  30158  iscref  30232  ordtrest2NEW  30290  fmcncfil  30298  issiga  30495  isrnsigaOLD  30496  isrnsiga  30497  isldsys  30540  ismeas  30583  carsgval  30686  issibf  30716  sitgfval  30724  signstfvneq0  30970  istrkg2d  31065  ispconn  31523  issconn  31526  txpconn  31532  cvxpconn  31542  cvmscbv  31558  iscvm  31559  cvmsdisj  31570  cvmsss2  31574  snmlval  31631  elmrsubrn  31735  ismfs  31764  mclsval  31778  frrlem4  32099  fwddifnval  32586  bj-ismoore  33365  poimirlem28  33745  cover2g  33816  seqpo  33849  incsequz2  33851  caushft  33863  ismtyval  33905  isass  33951  isexid  33952  elghomlem1OLD  33990  isrngo  34002  isrngod  34003  isgrpda  34060  rngohomval  34069  iscom2  34100  idlval  34118  pridlval  34138  maxidlval  34144  elrefrels3  34576  elcnvrefrels3  34589  lflset  34834  islfld  34837  isopos  34955  isoml  35013  isatl  35074  iscvlat  35098  ishlat1  35127  psubspset  35519  lautset  35857  pautsetN  35873  ldilfset  35883  ltrnfset  35892  dilfsetN  35927  trnfsetN  35930  trnsetN  35931  trlfset  35935  tendofset  36533  tendoset  36534  dihffval  37005  lpolsetN  37257  hdmapfval  37602  hgmapfval  37661  aomclem8  38126  islnm  38142  sdrgacs  38266  clsk1independent  38838  gneispace2  38924  gneispaceel2  38936  gneispacess2  38938  ioodvbdlimc1lem1  40620  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  issal  41007  isome  41184  iccpartiltu  41927  iccelpart  41938  isupwlk  42279  mgmpropd  42337  ismgmd  42338  ismgmhm  42345  resmgmhm  42360  iscllaw  42387  iscomlaw  42388  isasslaw  42390  isrng  42438  c0snmgmhm  42476  zlidlring  42490  uzlidlring  42491  dmatALTval  42751  islininds  42797  lindslinindsimp2  42814  ldepsnlinc  42859  elbigo  42907