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

Theorem raleqdv 3174
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
Hypothesis
Ref Expression
raleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
raleqdv (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv
StepHypRef Expression
1 raleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 raleq 3168 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 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:  raleqbidv  3182  raleqbidva  3184  raleleqALT  3187  raldifeq  4092  wfisg  5753  fveqressseq  6395  f12dfv  6569  f13dfv  6570  cbvfo  6584  isoselem  6631  ofrfval  6947  omsinds  7126  wfrlem4  7463  issmo2  7491  smoeq  7492  frfi  8246  marypha1lem  8380  marypha1  8381  dfoi  8457  oieq2  8459  ordtypecbv  8463  ordtypelem2  8465  ordtypelem3  8466  ordtypelem9  8472  wemapwe  8632  tcrank  8785  isacn  8905  pwsdompw  9064  isfin2  9154  isfin3ds  9189  isf33lem  9226  hsmexlem4  9289  zorn2lem6  9361  zorn2lem7  9362  zorn2g  9363  fpwwe2lem13  9502  uzsupss  11818  fzrevral2  12464  fzrevral3  12465  fzshftral  12466  fzoshftral  12625  uzsinds  12826  expmulnbnd  13036  eqs1  13429  swrdeq  13490  swrdspsleq  13495  2swrdeqwrdeq  13499  repswsymballbi  13573  cshw1  13614  wwlktovf1  13746  eqwrds3  13750  rexuz3  14132  rexuzre  14136  limsupgle  14252  rlim  14270  climconst  14318  rlimclim1  14320  climshftlem  14349  isercoll  14442  caucvgb  14454  serf0  14455  mertenslem1  14660  coprmprod  15422  coprmproddvds  15424  prmind2  15445  vdwlem10  15741  vdwlem13  15744  vdwnnlem2  15747  vdwnnlem3  15748  vdwnn  15749  ramval  15759  ramz  15776  prmgaplem5  15806  isacs  16359  cidpropd  16417  monpropd  16444  isssc  16527  fullsubc  16557  funcpropd  16607  isfth  16621  fthpropd  16628  grpidpropd  17308  mndpropd  17363  nmznsg  17685  ghmnsgima  17731  symgextfo  17888  gsmsymgrfixlem1  17893  gsmsymgrfix  17894  fvcosymgeq  17895  gsmsymgreqlem2  17897  symgfixf1  17903  psgnunilem3  17962  subgpgp  18058  sylow2blem3  18083  sylow3lem6  18093  efgsp1  18196  efgsres  18197  cmnpropd  18248  telgsumfzs  18432  ablfac2  18534  ringpropd  18628  abvpropd  18890  lsspropd  19065  lmhmpropd  19121  lbspropd  19147  pj1lmhm  19148  assapropd  19375  znf1o  19948  psgndiflemB  19994  phlpropd  20048  islindf  20199  lindfmm  20214  islindf4  20225  islindf5  20226  scmatf1  20385  isclo  20939  perfopn  21037  lmfval  21084  lmconst  21113  cncnp  21132  iscnrm2  21190  ist0-2  21196  ist1-2  21199  ishaus2  21203  ordtt1  21231  subislly  21332  elpt  21423  elptr  21424  ptbasfi  21432  tx1stc  21501  xkococnlem  21510  fclscmp  21881  ufilcmp  21883  cnpfcf  21892  alexsubALTlem1  21898  alexsubALTlem2  21899  alexsubALTlem4  21901  tmdgsum2  21947  tsmsf1o  21995  ustval  22053  ucnval  22128  imasdsf1olem  22225  imasf1oxmet  22227  imasf1omet  22228  metss  22360  prdsxmslem2  22381  cnmpt2pc  22774  lebnumlem3  22809  ishtpy  22818  pi1coghm  22907  lmnn  23107  evthicc  23274  cniccbdd  23276  ovolicc2lem4  23334  0pledm  23485  cniccibl  23652  c1lip1  23805  dvivthlem1  23816  lhop1  23822  itgsubstlem  23856  dgrlem  24030  ulmshftlem  24188  ulm0  24190  ulmcau  24194  iblulm  24206  rlimcnp  24737  xrlimcnp  24740  fsumdvdsmul  24966  chtub  24982  2sqlem10  25198  dchrisum0flb  25244  pntpbnd1  25320  pntpbnd  25322  pntibndlem2  25325  pntibndlem3  25326  pntibnd  25327  pntlemi  25338  pntleme  25342  pntlem3  25343  pntlemp  25344  pntleml  25345  pnt3  25346  istrkgld  25403  trgcgrg  25455  tgcgr4  25471  isperp  25652  brbtwn  25824  usgruspgrb  26121  usgr1e  26182  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nbgr0vtx  26297  nbgr1vtx  26299  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  cplgr1v  26382  cusgrexi  26395  1hevtxdg0  26457  wlkeq  26585  wlkl1loop  26590  uspgr2wlkeq  26598  upgr2wlk  26620  redwlk  26625  wlkp1lem8  26633  usgr2wlkneq  26708  usgr2trlncl  26712  usgr2pthlem  26715  usgr2pth  26716  pthdlem1  26718  uspgrn2crct  26756  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  wwlknp  26791  wwlksn0s  26815  wlkiswwlks1  26821  wlkiswwlks2lem4  26826  wlkiswwlksupgr2  26831  wlknewwlksn  26841  wwlksnred  26855  wwlksnext  26856  rusgrnumwwlkl1  26935  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a  26964  clwlkclwwlklem3  26967  clwwlkn  26985  clwwlknp  26999  clwwlkinwwlk  27003  clwwlkn1  27004  clwwlkn2  27007  clwwlkel  27009  clwwlkf  27010  clwwlkwwlksb  27018  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  clwlksfclwwlk  27049  clwlksf1clwwlklem  27055  clwwlknonex2  27084  1ewlk  27093  1wlkdlem4  27118  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  dfconngr1  27166  isconngr1  27168  frgr3v  27255  frgrwopregasn  27296  frgrwopregbsn  27297  clwwlkccatlem  27331  ubth  27857  acunirnmpt2  29588  acunirnmpt2f  29589  aciunf1  29591  lmxrge0  30126  sigaclcu3  30313  measval  30389  isrnmeas  30391  sitgval  30522  eulerpartlemsv3  30551  eulerpartlemo  30555  eulerpartlemn  30571  bnj1514  31257  subfacp1lem3  31290  subfacp1lem5  31292  txpconn  31340  cvxpconn  31350  cvmscbv  31366  cvmsi  31373  cvmsval  31374  elmrsubrn  31543  frpoinsg  31866  frinsg  31870  frrlem4  31908  bj-raldifsn  33179  poimirlem1  33540  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  heicant  33574  mblfinlem3  33578  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  cnicciblnc  33611  sdclem1  33669  fdc  33671  rrncmslem  33761  isass  33775  exidreslem  33806  exidresid  33808  isrngod  33827  isgrpda  33884  iscom2  33924  pautsetN  35702  tendofset  36363  tendoset  36364  hdmap14lem13  37489  kelac1  37950  gicabl  37986  lpirlnr  38004  fiinfi  38195  clsk1independent  38661  wessf1ornlem  39685  uzub  39971  mccl  40148  climsuse  40158  limsupmnfuzlem  40276  limsupmnfuz  40277  limsupre3uzlem  40285  limsupre3uz  40286  limsupreuz  40287  0cnv  40292  climuz  40294  lmbr3  40297  limsupgt  40328  liminflt  40355  xlimmnf  40385  xlimpnf  40386  xlimmnfmpt  40387  xlimpnfmpt  40388  dfxlim2  40392  fourierdlem2  40644  fourierdlem3  40645  fourierdlem31  40673  fourierdlem47  40688  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem80  40721  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  etransclem48  40817  etransc  40818  ismea  40986  caragenval  41028  omessle  41033  smfmullem2  41320  smfmul  41323  2ffzoeq  41663  iccpval  41676  iccpartigtl  41684  pfxeq  41729  pfxsuffeqwrdeq  41731  pfx2  41737  c0snmgmhm  42239  linds0  42579  lindsrng01  42582
  Copyright terms: Public domain W3C validator