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

Theorem raleqdv 3120
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 3114 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900
This theorem is referenced by:  raleqbidv  3128  raleqbidva  3130  raleleqALT  3133  raldifeq  4010  wfisg  5618  fveqressseq  6248  f12dfv  6407  f13dfv  6408  cbvfo  6422  isoselem  6469  ofrfval  6780  omsinds  6953  wfrlem4  7282  issmo2  7310  smoeq  7311  frfi  8067  marypha1lem  8199  marypha1  8200  dfoi  8276  oieq2  8278  ordtypecbv  8282  ordtypelem2  8284  ordtypelem3  8285  ordtypelem9  8291  wemapwe  8454  tcrank  8607  isacn  8727  pwsdompw  8886  isfin2  8976  isfin3ds  9011  isf33lem  9048  hsmexlem4  9111  zorn2lem6  9183  zorn2lem7  9184  zorn2g  9185  fpwwe2lem13  9320  uzsupss  11612  fzrevral2  12250  fzrevral3  12251  fzshftral  12252  fzoshftral  12402  uzsinds  12603  expmulnbnd  12813  eqs1  13191  swrdeq  13242  swrdspsleq  13247  2swrdeqwrdeq  13251  repswsymballbi  13324  cshw1  13365  wwlktovf1  13494  eqwrds3  13498  rexuz3  13882  rexuzre  13886  limsupgle  14002  rlim  14020  climconst  14068  rlimclim1  14070  climshftlem  14099  isercoll  14192  caucvgb  14204  serf0  14205  mertenslem1  14401  coprmprod  15159  coprmproddvds  15161  prmind2  15182  vdwlem10  15478  vdwlem13  15481  vdwnnlem2  15484  vdwnnlem3  15485  vdwnn  15486  ramval  15496  ramz  15513  prmgaplem5  15543  isacs  16081  cidpropd  16139  monpropd  16166  isssc  16249  fullsubc  16279  funcpropd  16329  isfth  16343  fthpropd  16350  grpidpropd  17030  mndpropd  17085  nmznsg  17407  ghmnsgima  17453  symgextfo  17611  gsmsymgrfixlem1  17616  gsmsymgrfix  17617  fvcosymgeq  17618  gsmsymgreqlem2  17620  symgfixf1  17626  psgnunilem3  17685  subgpgp  17781  sylow2blem3  17806  sylow3lem6  17816  efgsp1  17919  efgsres  17920  cmnpropd  17971  telgsumfzs  18155  ablfac2  18257  ringpropd  18351  abvpropd  18611  lsspropd  18784  lmhmpropd  18840  lbspropd  18866  pj1lmhm  18867  assapropd  19094  znf1o  19664  psgndiflemB  19710  phlpropd  19764  islindf  19912  lindfmm  19927  islindf4  19938  islindf5  19939  scmatf1  20098  isclo  20643  perfopn  20741  lmfval  20788  lmconst  20817  cncnp  20836  iscnrm2  20894  ist0-2  20900  ist1-2  20903  ishaus2  20907  ordtt1  20935  subislly  21036  elpt  21127  elptr  21128  ptbasfi  21136  tx1stc  21205  xkococnlem  21214  fclscmp  21586  ufilcmp  21588  cnpfcf  21597  alexsubALTlem1  21603  alexsubALTlem2  21604  alexsubALTlem4  21606  tmdgsum2  21652  tsmsf1o  21700  ustval  21758  ucnval  21833  imasdsf1olem  21929  imasf1oxmet  21931  imasf1omet  21932  metss  22064  prdsxmslem2  22085  cnmpt2pc  22466  lebnumlem3  22501  ishtpy  22510  pi1coghm  22600  lmnn  22787  evthicc  22952  cniccbdd  22954  ovolicc2lem4  23012  0pledm  23163  cniccibl  23330  c1lip1  23481  dvivthlem1  23492  lhop1  23498  itgsubstlem  23532  dgrlem  23706  ulmshftlem  23864  ulm0  23866  ulmcau  23870  iblulm  23882  rlimcnp  24409  xrlimcnp  24412  fsumdvdsmul  24638  chtub  24654  2sqlem10  24870  dchrisum0flb  24916  pntpbnd1  24992  pntpbnd  24994  pntibndlem2  24997  pntibndlem3  24998  pntibnd  24999  pntlemi  25010  pntleme  25014  pntlem3  25015  pntlemp  25016  pntleml  25017  pnt3  25018  istrkgld  25075  trgcgrg  25128  tgcgr4  25144  isperp  25325  brbtwn  25497  cusgra2v  25757  cusgra3v  25759  uvtxnb  25791  is2wlk  25861  constr1trl  25884  constr2wlk  25894  constr2trl  25895  redwlk  25902  usgra2wlkspthlem1  25913  usgra2wlkspthlem2  25914  usgrcyclnl2  25935  3v3e3cycl1  25938  constr3trllem2  25945  constr3trllem5  25948  4cycl4v4e  25960  4cycl4dv4e  25962  dfconngra1  25965  wwlknimp  25981  wlkiswwlk1  25984  wlkiswwlk2lem4  25988  wwlkn0s  25999  vfwlkniswwlkn  26000  2wlkeq  26001  usg2wlkeq  26002  wwlknred  26017  wwlknext  26018  clwwlkn2  26069  clwwlknimp  26070  clwlkisclwwlklem2a1  26073  clwlkisclwwlklem2a  26079  clwlkisclwwlklem0  26082  clwwlkel  26087  clwwlkf  26088  wwlkext2clwwlk  26097  wwlksubclwwlk  26098  clwlkfclwwlk  26137  clwlkf1clwwlklem  26142  rusgranumwlkl1  26240  rusgra0edg  26248  eupai  26260  eupatrl  26261  eupa0  26267  eupares  26268  eupap1  26269  frgra3v  26295  frgrawopreg1  26343  extwwlkfablem2  26371  numclwwlkovf2ex  26379  ubth  26919  acunirnmpt2  28648  acunirnmpt2f  28649  aciunf1  28651  lmxrge0  29132  sigaclcu3  29318  measval  29394  isrnmeas  29396  sitgval  29527  eulerpartlemsv3  29556  eulerpartlemo  29560  eulerpartlemn  29576  bnj1514  30191  subfacp1lem3  30224  subfacp1lem5  30226  txpcon  30274  cvxpcon  30284  cvmscbv  30300  cvmsi  30307  cvmsval  30308  elmrsubrn  30477  frinsg  30792  poimirlem1  32383  poimirlem26  32408  poimirlem27  32409  poimirlem31  32413  poimirlem32  32414  heicant  32417  mblfinlem3  32421  ovoliunnfl  32424  voliunnfl  32426  volsupnfl  32427  cnicciblnc  32454  sdclem1  32512  fdc  32514  rrncmslem  32604  isass  32618  exidreslem  32649  exidresid  32651  isrngod  32670  isgrpda  32727  iscom2  32767  pautsetN  34205  tendofset  34867  tendoset  34868  hdmap14lem13  35993  kelac1  36454  gicabl  36490  lpirlnr  36509  fiinfi  36700  clsk1independent  37167  wessf1ornlem  38169  mccl  38469  climsuse  38479  fourierdlem2  38806  fourierdlem3  38807  fourierdlem31  38835  fourierdlem47  38850  fourierdlem70  38873  fourierdlem71  38874  fourierdlem73  38876  fourierdlem80  38883  fourierdlem103  38906  fourierdlem104  38907  fourierdlem113  38916  etransclem48  38979  etransc  38980  issal  39014  ismea  39148  caragenval  39187  isome  39188  omessle  39192  smfmullem2  39481  smfmul  39484  iccpval  39758  iccpartigtl  39766  pfxeq  40072  pfxsuffeqwrdeq  40074  pfx2  40080  2ffzoeq  40188  usgruspgrb  40413  usgr1e  40473  nbgr2vtx1edg  40574  nbuhgr2vtx1edgb  40576  nbgr0vtx  40580  nbgr1vtx  40582  uvtxa01vtx0  40625  cplgr1v  40654  cusgrexi  40664  1hevtxdg0  40722  1wlkeq  40840  1wlkl1loop  40844  uspgr2wlkeq  40856  upgr2wlk  40878  red1wlk  40883  1wlkp1lem8  40891  usgr2wlkneq  40964  usgr2trlncl  40968  usgr2pthlem  40971  usgr2pth  40972  pthdlem1  40974  uspgrn2crct  41013  crctcsh1wlkn0lem7  41021  crctcsh1wlkn0  41026  wwlknp  41047  wwlksn0s  41059  1wlkiswwlks1  41066  1wlkiswwlks2lem4  41071  1wlkiswwlksupgr2  41076  wlknewwlksn  41086  wwlksnred  41100  wwlksnext  41101  rusgrnumwwlkl1  41174  clwwlknp  41197  clwlkclwwlklem2a1  41203  clwlkclwwlklem2a  41209  clwlkclwwlklem3  41212  clwwlksn2  41219  clwwlksel  41223  clwwlksf  41224  wwlksext2clwwlk  41233  wwlksubclwwlks  41234  clwlksfclwwlk  41271  clwlksf1clwwlklem  41277  1ewlk  41285  11wlkdlem4  41309  upgr3v3e3cycl  41349  upgr4cycl4dv4e  41354  dfconngr1  41357  isconngr1  41359  frgr1v  41443  frgr3v  41447  frgrwopreg1  41489  av-numclwwlkovf2ex  41519  c0snmgmhm  41706  linds0  42050  lindsrng01  42053
  Copyright terms: Public domain W3C validator