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

Theorem raleqdv 3137
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 3131 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  raleqbidv  3145  raleqbidva  3147  raleleqALT  3150  raldifeq  4037  wfisg  5684  fveqressseq  6321  f12dfv  6494  f13dfv  6495  cbvfo  6509  isoselem  6556  ofrfval  6870  omsinds  7046  wfrlem4  7378  issmo2  7406  smoeq  7407  frfi  8165  marypha1lem  8299  marypha1  8300  dfoi  8376  oieq2  8378  ordtypecbv  8382  ordtypelem2  8384  ordtypelem3  8385  ordtypelem9  8391  wemapwe  8554  tcrank  8707  isacn  8827  pwsdompw  8986  isfin2  9076  isfin3ds  9111  isf33lem  9148  hsmexlem4  9211  zorn2lem6  9283  zorn2lem7  9284  zorn2g  9285  fpwwe2lem13  9424  uzsupss  11740  fzrevral2  12383  fzrevral3  12384  fzshftral  12385  fzoshftral  12541  uzsinds  12742  expmulnbnd  12952  eqs1  13347  swrdeq  13398  swrdspsleq  13403  2swrdeqwrdeq  13407  repswsymballbi  13480  cshw1  13521  wwlktovf1  13650  eqwrds3  13654  rexuz3  14038  rexuzre  14042  limsupgle  14158  rlim  14176  climconst  14224  rlimclim1  14226  climshftlem  14255  isercoll  14348  caucvgb  14360  serf0  14361  mertenslem1  14560  coprmprod  15318  coprmproddvds  15320  prmind2  15341  vdwlem10  15637  vdwlem13  15640  vdwnnlem2  15643  vdwnnlem3  15644  vdwnn  15645  ramval  15655  ramz  15672  prmgaplem5  15702  isacs  16252  cidpropd  16310  monpropd  16337  isssc  16420  fullsubc  16450  funcpropd  16500  isfth  16514  fthpropd  16521  grpidpropd  17201  mndpropd  17256  nmznsg  17578  ghmnsgima  17624  symgextfo  17782  gsmsymgrfixlem1  17787  gsmsymgrfix  17788  fvcosymgeq  17789  gsmsymgreqlem2  17791  symgfixf1  17797  psgnunilem3  17856  subgpgp  17952  sylow2blem3  17977  sylow3lem6  17987  efgsp1  18090  efgsres  18091  cmnpropd  18142  telgsumfzs  18326  ablfac2  18428  ringpropd  18522  abvpropd  18782  lsspropd  18957  lmhmpropd  19013  lbspropd  19039  pj1lmhm  19040  assapropd  19267  znf1o  19840  psgndiflemB  19886  phlpropd  19940  islindf  20091  lindfmm  20106  islindf4  20117  islindf5  20118  scmatf1  20277  isclo  20831  perfopn  20929  lmfval  20976  lmconst  21005  cncnp  21024  iscnrm2  21082  ist0-2  21088  ist1-2  21091  ishaus2  21095  ordtt1  21123  subislly  21224  elpt  21315  elptr  21316  ptbasfi  21324  tx1stc  21393  xkococnlem  21402  fclscmp  21774  ufilcmp  21776  cnpfcf  21785  alexsubALTlem1  21791  alexsubALTlem2  21792  alexsubALTlem4  21794  tmdgsum2  21840  tsmsf1o  21888  ustval  21946  ucnval  22021  imasdsf1olem  22118  imasf1oxmet  22120  imasf1omet  22121  metss  22253  prdsxmslem2  22274  cnmpt2pc  22667  lebnumlem3  22702  ishtpy  22711  pi1coghm  22801  lmnn  23001  evthicc  23168  cniccbdd  23170  ovolicc2lem4  23228  0pledm  23380  cniccibl  23547  c1lip1  23698  dvivthlem1  23709  lhop1  23715  itgsubstlem  23749  dgrlem  23923  ulmshftlem  24081  ulm0  24083  ulmcau  24087  iblulm  24099  rlimcnp  24626  xrlimcnp  24629  fsumdvdsmul  24855  chtub  24871  2sqlem10  25087  dchrisum0flb  25133  pntpbnd1  25209  pntpbnd  25211  pntibndlem2  25214  pntibndlem3  25215  pntibnd  25216  pntlemi  25227  pntleme  25231  pntlem3  25232  pntlemp  25233  pntleml  25234  pnt3  25235  istrkgld  25292  trgcgrg  25344  tgcgr4  25360  isperp  25541  brbtwn  25713  usgruspgrb  26003  usgr1e  26064  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  nbgr0vtx  26173  nbgr1vtx  26175  uvtxa01vtx0  26218  cplgr1v  26247  cusgrexi  26260  1hevtxdg0  26321  wlkeq  26433  wlkl1loop  26437  uspgr2wlkeq  26445  upgr2wlk  26467  redwlk  26472  wlkp1lem8  26480  usgr2wlkneq  26555  usgr2trlncl  26559  usgr2pthlem  26562  usgr2pth  26563  pthdlem1  26565  uspgrn2crct  26603  crctcshwlkn0lem7  26611  crctcshwlkn0  26616  wwlknp  26637  wwlksn0s  26649  wlkiswwlks1  26656  wlkiswwlks2lem4  26661  wlkiswwlksupgr2  26666  wlknewwlksn  26676  wwlksnred  26690  wwlksnext  26691  rusgrnumwwlkl1  26764  clwwlknp  26788  clwlkclwwlklem2a1  26794  clwlkclwwlklem2a  26800  clwlkclwwlklem3  26803  clwwlksn2  26810  clwwlksel  26814  clwwlksf  26815  wwlksext2clwwlk  26824  wwlksubclwwlks  26825  clwlksfclwwlk  26862  clwlksf1clwwlklem  26868  1ewlk  26876  1wlkdlem4  26900  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  dfconngr1  26948  isconngr1  26950  frgr3v  27037  frgrwopreg1  27079  numclwwlkovf2ex  27109  ubth  27617  acunirnmpt2  29343  acunirnmpt2f  29344  aciunf1  29346  lmxrge0  29822  sigaclcu3  30008  measval  30084  isrnmeas  30086  sitgval  30217  eulerpartlemsv3  30246  eulerpartlemo  30250  eulerpartlemn  30266  bnj1514  30892  subfacp1lem3  30925  subfacp1lem5  30927  txpconn  30975  cvxpconn  30985  cvmscbv  31001  cvmsi  31008  cvmsval  31009  elmrsubrn  31178  frinsg  31496  poimirlem1  33081  poimirlem26  33106  poimirlem27  33107  poimirlem31  33111  poimirlem32  33112  heicant  33115  mblfinlem3  33119  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  cnicciblnc  33152  sdclem1  33210  fdc  33212  rrncmslem  33302  isass  33316  exidreslem  33347  exidresid  33349  isrngod  33368  isgrpda  33425  iscom2  33465  pautsetN  34903  tendofset  35565  tendoset  35566  hdmap14lem13  36691  kelac1  37152  gicabl  37188  lpirlnr  37207  fiinfi  37398  clsk1independent  37865  wessf1ornlem  38880  uzub  39157  mccl  39266  climsuse  39276  limsupmnfuzlem  39394  limsupmnfuz  39395  limsupre3uzlem  39403  limsupre3uz  39404  limsupreuz  39405  fourierdlem2  39663  fourierdlem3  39664  fourierdlem31  39692  fourierdlem47  39707  fourierdlem70  39730  fourierdlem71  39731  fourierdlem73  39733  fourierdlem80  39740  fourierdlem103  39763  fourierdlem104  39764  fourierdlem113  39773  etransclem48  39836  etransc  39837  ismea  40005  caragenval  40044  omessle  40049  smfmullem2  40336  smfmul  40339  2ffzoeq  40665  iccpval  40679  iccpartigtl  40687  pfxeq  40733  pfxsuffeqwrdeq  40735  pfx2  40741  c0snmgmhm  41232  linds0  41572  lindsrng01  41575
  Copyright terms: Public domain W3C validator