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

Theorem cbvralv 3147
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
Hypothesis
Ref Expression
cbvralv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralv (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralv
StepHypRef Expression
1 nfv 1830 . 2 𝑦𝜑
2 nfv 1830 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3143 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901
This theorem is referenced by:  cbvral2v  3155  cbvral3v  3157  reu7  3368  disjxun  4581  reusv3i  4801  wereu2  5035  cnvpo  5590  f1mpt  6419  grprinvlem  6770  grprinvd  6771  dfwe2  6873  tfinds  6951  wfrlem1  7301  tfrlem1  7359  tfrlem12  7372  rdglem1  7398  tz7.48lem  7423  nneneq  8028  marypha1lem  8222  supub  8248  suplub  8249  ordtypecbv  8305  ordtypelem3  8308  ordtypelem9  8314  wemaplem1  8334  brwdom3  8370  tcrank  8630  infxpenc2  8728  aceq1  8823  aceq2  8825  dfac5  8834  dfac9  8841  dfac12lem3  8850  kmlem12  8866  kmlem14  8868  cofsmo  8974  infpssrlem4  9011  isfin3ds  9034  isf32lem2  9059  isf32lem11  9068  isf33lem  9071  domtriomlem  9147  axdc3  9159  zorn2lem7  9207  zorn2g  9208  fpwwe2cbv  9331  fpwwecbv  9345  pwfseq  9365  axgroth6  9529  dedekind  10079  suprleub  10866  infregelb  10884  nnsub  10936  uzwo  11627  ublbneg  11649  zsupss  11653  xrub  12014  fsuppmapnn0fiubex  12654  monoord2  12694  faclbnd4lem4  12945  bccl  12971  hashbc  13094  wrdind  13328  wrd2ind  13329  reuccats1  13332  cau3lem  13942  climmpt2  14152  caucvgrlem  14251  caurcvg2  14256  caucvgb  14258  fsum0diag2  14357  incexclem  14407  cvgrat  14454  mertenslem2  14456  mertens  14457  sqrt2irr  14817  gcdcllem1  15059  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  prmind2  15236  prmpwdvds  15446  prmreclem5  15462  prmreclem6  15463  vdwlem7  15529  vdwlem10  15532  vdwlem13  15535  vdwnn  15540  ramcl  15571  isacs2  16137  catpropd  16192  gsumvalx  17093  mrcmndind  17189  issubg4  17436  isnsg2  17447  elnmz  17456  gsmsymgreqlem2  17674  psgnunilem5  17737  psgnunilem3  17739  efgsdm  17966  gsummptnn0fzfv  18207  pgpfac1lem5  18301  pgpfac1  18302  pgpfac  18306  ablfaclem3  18309  lbsextg  18983  evlslem2  19333  mpfind  19357  cply1mul  19485  mdetuni0  20246  m2cpminvid2lem  20378  mp2pm2mplem4  20433  chcoeffeqlem  20509  cayhamlem3  20511  elcls3  20697  isclo2  20702  neiptopnei  20746  tgcn  20866  subbascn  20868  txcmplem2  21255  kqfvima  21343  kqt0lem  21349  isr0  21350  r0cld  21351  regr1lem2  21353  fbun  21454  flftg  21610  fclsbas  21635  alexsubALTlem2  21662  alexsubALTlem4  21664  ptcmplem4  21669  tsmsxplem1  21766  tsmsxp  21768  ustuqtop  21860  utopsnneip  21862  prdsxmslem2  22144  isclmp  22705  iscau4  22885  caucfil  22889  iscmet3  22899  bcthlem5  22933  bcth  22934  ovolicc2lem5  23096  uniioombllem6  23162  vitali  23188  ismbf3d  23227  itg1climres  23287  itg2seq  23315  itg2monolem1  23323  itg2mono  23326  rolle  23557  dvlipcn  23561  dvivthlem1  23575  ply1divex  23700  fta1g  23731  dgrco  23835  plydivex  23856  fta1  23867  vieta1  23871  ulmcaulem  23952  ulmcau  23953  abelthlem8  23997  wilth  24597  fta  24606  dchrelbas3  24763  2sqlem6  24948  2sqlem10  24953  dchrisumlem3  24980  dchrisum  24981  dchrmusumlema  24982  dchrvmasumlema  24989  dchrisum0lema  25003  pntibndlem3  25081  pntlem3  25098  pntleml  25100  pnt3  25101  ostth2lem2  25123  ostth  25128  axcontlem1  25644  axcontlem6  25649  cusgrafilem2  26008  usg2wlkeq  26236  grpoideu  26747  ubthlem3  27112  adjsym  28076  lnopunilem1  28253  elunop2  28256  lnophm  28262  cnlnadjlem5  28314  mdbr3  28540  mdbr4  28541  dmdbr3  28548  dmdbr4  28549  mddmd2  28552  toslublem  28998  tosglblem  29000  archiabl  29083  isarchiofld  29148  qtophaus  29231  lmdvg  29327  esumcvg  29475  unelldsys  29548  ldgenpisyslem1  29553  eulerpartlemsv3  29750  eulerpartlemgvv  29765  signstfvneq0  29975  bnj1185  30118  bnj1379  30155  bnj222  30207  bnj517  30209  bnj1450  30372  bnj1452  30374  bnj1463  30377  derangenlem  30407  subfacp1lem6  30421  subfacp1  30422  rescon  30482  cvmscbv  30494  untangtr  30845  dfon2lem3  30934  dfon2lem7  30938  frrlem1  31024  nn0prpwlem  31487  neibastop3  31527  fnemeet2  31532  phpreu  32563  poimirlem27  32606  heicant  32614  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  mbfresfi  32626  upixp  32694  sdclem2  32708  fdc  32711  mettrifi  32723  heiborlem5  32784  heiborlem10  32789  heibor  32790  bfp  32793  cdleme25cv  34664  cdleme40v  34775  mzpclval  36306  dford3lem1  36611  fnwe2lem1  36638  aomclem3  36644  aomclem4  36645  aomclem8  36649  dfac11  36650  hbtlem5  36717  ntrk2imkb  37355  ntrclsk2  37386  ntrclsk4  37390  fnchoice  38211  cncmpmax  38214  wessf1ornlem  38366  disjinfi  38375  mccl  38665  climsuse  38675  limsupre  38708  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem3  38838  stoweidlem7  38900  stoweidlem15  38908  stoweidlem35  38928  wallispilem3  38960  fourierdlem68  39067  fourierdlem71  39070  fourierdlem73  39072  fourierdlem87  39086  fourierdlem100  39099  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem109  39108  fourierdlem112  39111  etransc  39176  qndenserrnbllem  39190  dfsalgen2  39235  subsaliuncl  39252  meaiuninclem  39373  ovnsubaddlem2  39461  hoidmvlelem5  39489  hoidmvle  39490  hoiqssbllem3  39514  vonioo  39573  vonicc  39576  issmf  39614  issmfle  39632  issmfgt  39643  issmfge  39656  bgoldbtbndlem4  40224  bgoldbtbnd  40225  uspgr2wlkeq  40854  crctcsh1wlkn0  41024  nn0sumshdiglem1  42213
  Copyright terms: Public domain W3C validator