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

Theorem raleqbi1dv 3135
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Hypothesis
Ref Expression
raleqd.1 (𝐴 = 𝐵 → (𝜑𝜓))
Assertion
Ref Expression
raleqbi1dv (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 raleq 3127 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
2 raleqd.1 . . 3 (𝐴 = 𝐵 → (𝜑𝜓))
32ralbidv 2980 . 2 (𝐴 = 𝐵 → (∀𝑥𝐵 𝜑 ↔ ∀𝑥𝐵 𝜓))
41, 3bitrd 268 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wral 2907
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 2912
This theorem is referenced by:  isoeq4  6527  wfrlem1  7362  wfrlem4  7366  wfrlem15  7377  smo11  7409  dffi2  8276  inficl  8278  dffi3  8284  dfom3  8491  aceq1  8887  dfac5lem4  8896  kmlem1  8919  kmlem10  8928  kmlem13  8931  kmlem14  8932  cofsmo  9038  infpssrlem4  9075  axdc3lem2  9220  elwina  9455  elina  9456  iswun  9473  eltskg  9519  elgrug  9561  elnp  9756  elnpi  9757  dfnn2  10980  dfnn3  10981  dfuzi  11415  coprmprod  15302  coprmproddvds  15304  ismri  16215  isprs  16854  isdrs  16858  ispos  16871  istos  16959  pospropd  17058  isipodrs  17085  isdlat  17117  mhmpropd  17265  issubm  17271  subgacs  17553  nsgacs  17554  isghm  17584  ghmeql  17607  iscmn  18124  dfrhm2  18641  islss  18857  lssacs  18889  lmhmeql  18977  islbs  18998  lbsextlem1  19080  lbsextlem3  19082  lbsextlem4  19083  isobs  19986  mat0dimcrng  20198  istopg  20622  isbasisg  20665  basis2  20669  eltg2  20676  iscldtop  20812  neipeltop  20846  isreg  21049  regsep  21051  isnrm  21052  islly  21184  isnlly  21185  llyi  21190  nllyi  21191  islly2  21200  cldllycmp  21211  isfbas  21546  fbssfi  21554  isust  21920  elutop  21950  ustuqtop  21963  utopsnneip  21965  ispsmet  22022  ismet  22041  isxmet  22042  metrest  22242  cncfval  22604  fmcfil  22983  iscfil3  22984  caucfil  22994  iscmet3  23004  cfilres  23007  minveclem3  23113  wilthlem2  24702  wilthlem3  24703  wilth  24704  dfconngr1  26921  isconngr  26922  isplig  27189  isplig2  27190  isgrpo  27212  isablo  27261  disjabrex  29252  disjabrexf  29253  isomnd  29498  isorng  29596  isrnsigaOLD  29968  isrnsiga  29969  isldsys  30012  isros  30024  issros  30031  bnj1286  30816  bnj1452  30849  kur14lem9  30925  cvmscbv  30969  cvmsi  30976  cvmsval  30977  frrlem1  31502  frrlem4  31505  neibastop1  32017  neibastop2lem  32018  neibastop2  32019  isbnd  33232  ismndo2  33326  rngomndo  33387  isidl  33466  ispsubsp  34532  isnacs  36768  mzpclval  36789  elmzpcl  36790  mgmhmpropd  41089  issubmgm  41093  rnghmval  41195  zrrnghm  41221
  Copyright terms: Public domain W3C validator