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

Theorem raleqdv 3413
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 3403 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  raleqbidvOLD  3421  raleqbidva  3423  raleleqALT  3426  raldifeq  4435  wfisg  6176  fveqressseq  6839  f12dfv  7021  f13dfv  7022  cbvfo  7036  isoselem  7083  ofrfval  7406  omsinds  7589  wfrlem4  7947  issmo2  7975  smoeq  7976  frfi  8751  marypha1lem  8885  marypha1  8886  dfoi  8963  oieq2  8965  ordtypecbv  8969  ordtypelem2  8971  ordtypelem3  8972  ordtypelem9  8978  wemapwe  9148  tcrank  9301  isacn  9458  pwsdompw  9614  isfin2  9704  isfin3ds  9739  isf33lem  9776  hsmexlem4  9839  zorn2lem6  9911  zorn2lem7  9912  zorn2g  9913  fpwwe2lem13  10052  uzsupss  12328  fzrevral2  12981  fzrevral3  12982  fzshftral  12983  fzoshftral  13142  uzsinds  13343  expmulnbnd  13584  eqs1  13954  swrdspsleq  14015  pfxeq  14046  pfxsuffeqwrdeq  14048  repswsymballbi  14130  cshw1  14172  pfx2  14297  wwlktovf1  14309  eqwrds3  14313  rexuz3  14696  rexuzre  14700  limsupgle  14822  rlim  14840  climconst  14888  rlimclim1  14890  climshftlem  14919  isercoll  15012  caucvgb  15024  serf0  15025  mertenslem1  15228  coprmprod  15993  coprmproddvds  15995  prmind2  16017  vdwlem10  16314  vdwlem13  16317  vdwnnlem2  16320  vdwnnlem3  16321  vdwnn  16322  ramval  16332  ramz  16349  prmgaplem5  16379  isacs  16910  cidpropd  16968  monpropd  16995  isssc  17078  fullsubc  17108  funcpropd  17158  isfth  17172  fthpropd  17179  grpidpropd  17860  mndpropd  17924  nmznsg  18258  ghmnsgima  18320  symgextfo  18479  gsmsymgrfixlem1  18484  gsmsymgrfix  18485  fvcosymgeq  18486  gsmsymgreqlem2  18488  symgfixf1  18494  psgnunilem3  18553  subgpgp  18651  sylow2blem3  18676  sylow3lem6  18686  efgsp1  18792  efgsres  18793  cmnpropd  18845  telgsumfzs  19038  ablfac2  19140  ringpropd  19261  abvpropd  19542  lsspropd  19718  lmhmpropd  19774  lbspropd  19800  pj1lmhm  19801  assapropd  20029  znf1o  20626  psgndiflemB  20672  phlpropd  20727  islindf  20884  lindfmm  20899  islindf4  20910  islindf5  20911  scmatf1  21068  isclo  21623  perfopn  21721  lmfval  21768  lmconst  21797  cncnp  21816  iscnrm2  21874  ist0-2  21880  ist1-2  21883  ishaus2  21887  ordtt1  21915  subislly  22017  elpt  22108  elptr  22109  ptbasfi  22117  tx1stc  22186  xkococnlem  22195  fclscmp  22566  ufilcmp  22568  cnpfcf  22577  alexsubALTlem1  22583  alexsubALTlem2  22584  alexsubALTlem4  22586  tmdgsum2  22632  tsmsf1o  22680  ustval  22738  ucnval  22813  imasdsf1olem  22910  imasf1oxmet  22912  imasf1omet  22913  metss  23045  prdsxmslem2  23066  cnmpopc  23459  lebnumlem3  23494  ishtpy  23503  pi1coghm  23592  lmnn  23793  evthicc  23987  cniccbdd  23989  ovolicc2lem4  24048  0pledm  24201  cniccibl  24368  c1lip1  24521  dvivthlem1  24532  lhop1  24538  itgsubstlem  24572  dgrlem  24746  ulmshftlem  24904  ulm0  24906  ulmcau  24910  iblulm  24922  rlimcnp  25470  xrlimcnp  25473  fsumdvdsmul  25699  chtub  25715  2sqlem10  25931  dchrisum0flb  26013  pntpbnd1  26089  pntpbnd  26091  pntibndlem2  26094  pntibndlem3  26095  pntibnd  26096  pntlemi  26107  pntleme  26111  pntlem3  26112  pntlemp  26113  pntleml  26114  pnt3  26115  istrkgld  26172  trgcgrg  26228  tgcgr4  26244  isperp  26425  brbtwn  26612  usgruspgrb  26893  usgr1e  26954  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  nbgr0vtx  27065  nbgr1vtx  27067  uvtx01vtx  27106  cplgr1v  27139  cusgrexi  27152  1hevtxdg0  27214  wlkeq  27342  wlkl1loop  27346  uspgr2wlkeq  27354  upgr2wlk  27377  redwlk  27381  wlkp1lem8  27389  usgr2wlkneq  27464  usgr2trlncl  27468  usgr2pthlem  27471  usgr2pth  27472  pthdlem1  27474  uspgrn2crct  27513  crctcshwlkn0lem7  27521  crctcshwlkn0  27526  wwlknp  27548  wwlksn0s  27566  wlkiswwlks1  27572  wlkiswwlks2lem4  27577  wlkiswwlksupgr2  27582  wlknewwlksn  27592  wwlksnred  27597  wwlksnext  27598  rusgrnumwwlkl1  27674  clwwlkccatlem  27694  clwlkclwwlklem2a1  27697  clwlkclwwlklem2a  27703  clwlkclwwlklem3  27706  clwlkclwwlkf1lem3  27711  clwwlkn  27731  clwwlknp  27742  clwwlkinwwlk  27745  clwwlkn1  27746  clwwlkn2  27749  clwwlkel  27752  clwwlkf  27753  clwwlkwwlksb  27760  wwlksext2clwwlk  27763  wwlksubclwwlk  27764  clwwlknonex2  27815  1ewlk  27821  1wlkdlem4  27846  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  dfconngr1  27894  isconngr1  27896  frgr3v  27981  frgrwopregasn  28022  frgrwopregbsn  28023  ubth  28577  acunirnmpt2  30333  acunirnmpt2f  30334  aciunf1  30336  fnpreimac  30344  lmxrge0  31094  sigaclcu3  31280  measval  31356  isrnmeas  31358  sitgval  31489  eulerpartlemsv3  31518  eulerpartlemo  31522  eulerpartlemn  31538  bnj1514  32232  subfacp1lem3  32326  subfacp1lem5  32328  txpconn  32376  cvxpconn  32386  cvmscbv  32402  cvmsi  32409  cvmsval  32410  satf  32497  sat1el2xp  32523  elmrsubrn  32664  frpoinsg  32978  frinsg  32984  frrlem4  33023  bj-raldifsn  34286  poimirlem1  34774  poimirlem26  34799  poimirlem27  34800  poimirlem31  34804  poimirlem32  34805  heicant  34808  mblfinlem3  34812  ovoliunnfl  34815  voliunnfl  34817  volsupnfl  34818  cnicciblnc  34844  sdclem1  34899  fdc  34901  rrncmslem  34991  isass  35005  exidreslem  35036  exidresid  35038  isrngod  35057  isgrpda  35114  iscom2  35154  pautsetN  37114  tendofset  37774  tendoset  37775  hdmap14lem13  38896  kelac1  39541  gicabl  39577  lpirlnr  39595  fiinfi  39810  clsk1independent  40274  scotteqd  40450  wessf1ornlem  41321  uzub  41581  mccl  41755  climsuse  41765  limsupmnfuzlem  41883  limsupmnfuz  41884  limsupre3uzlem  41892  limsupre3uz  41893  limsupreuz  41894  0cnv  41899  climuz  41901  lmbr3  41904  limsupgt  41935  liminflt  41962  xlimpnfxnegmnf  41971  xlimmnf  41998  xlimpnf  41999  xlimmnfmpt  42000  xlimpnfmpt  42001  dfxlim2  42005  fourierdlem2  42271  fourierdlem3  42272  fourierdlem31  42300  fourierdlem47  42315  fourierdlem70  42338  fourierdlem71  42339  fourierdlem73  42341  fourierdlem80  42348  fourierdlem103  42371  fourierdlem104  42372  fourierdlem113  42381  etransclem48  42444  etransc  42445  caragenval  42652  omessle  42657  smfmullem2  42944  smfmul  42947  2ffzoeq  43405  iccpval  43452  iccpartigtl  43460  c0snmgmhm  44113  linds0  44448  lindsrng01  44451  rrx2line  44655
  Copyright terms: Public domain W3C validator