Theorem cbvralv 3171

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

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 3167	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  cbvral2v  3179  cbvral3v  3181  reu7  3401  disjxun  4651  reusv3i  4875  wereu2  5111  cnvpo  5673  f1mpt  6518  grprinvlem  6872  grprinvd  6873  dfwe2  6981  tfinds  7059  wfrlem1  7414  tfrlem1  7472  tfrlem12  7485  rdglem1  7511  tz7.48lem  7536  nneneq  8143  marypha1lem  8339  supub  8365  suplub  8366  ordtypecbv  8422  ordtypelem3  8425  ordtypelem9  8431  wemaplem1  8451  brwdom3  8487  tcrank  8747  infxpenc2  8845  aceq1  8940  aceq2  8942  dfac5  8951  dfac9  8958  dfac12lem3  8967  kmlem12  8983  kmlem14  8985  cofsmo  9091  infpssrlem4  9128  isfin3ds  9151  isf32lem2  9176  isf32lem11  9185  isf33lem  9188  domtriomlem  9264  axdc3  9276  zorn2lem7  9324  zorn2g  9325  fpwwe2cbv  9452  fpwwecbv  9466  pwfseq  9486  axgroth6  9650  dedekind  10200  suprleub  10989  infregelb  11007  nnsub  11059  uzwo  11751  ublbneg  11773  zsupss  11777  xrub  12142  fsuppmapnn0fiubex  12792  monoord2  12832  faclbnd4lem4  13083  bccl  13109  hashbc  13237  wrdind  13476  wrd2ind  13477  reuccats1  13480  cau3lem  14094  climmpt2  14304  caucvgrlem  14403  caurcvg2  14408  caucvgb  14410  fsum0diag2  14515  incexclem  14568  cvgrat  14615  mertenslem2  14617  mertens  14618  sqrt2irr  14979  gcdcllem1  15221  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  prmind2  15398  prmpwdvds  15608  prmreclem5  15624  prmreclem6  15625  vdwlem7  15691  vdwlem10  15694  vdwlem13  15697  vdwnn  15702  ramcl  15733  isacs2  16314  catpropd  16369  gsumvalx  17270  mrcmndind  17366  issubg4  17613  isnsg2  17624  elnmz  17633  gsmsymgreqlem2  17851  psgnunilem5  17914  psgnunilem3  17916  efgsdm  18143  gsummptnn0fzfv  18384  pgpfac1lem5  18478  pgpfac1  18479  pgpfac  18483  ablfaclem3  18486  lbsextg  19162  evlslem2  19512  mpfind  19536  cply1mul  19664  mdetuni0  20427  m2cpminvid2lem  20559  mp2pm2mplem4  20614  chcoeffeqlem  20690  cayhamlem3  20692  elcls3  20887  isclo2  20892  neiptopnei  20936  tgcn  21056  subbascn  21058  txcmplem2  21445  kqfvima  21533  kqt0lem  21539  isr0  21540  r0cld  21541  regr1lem2  21543  fbun  21644  flftg  21800  fclsbas  21825  alexsubALTlem2  21852  alexsubALTlem4  21854  ptcmplem4  21859  tsmsxplem1  21956  tsmsxp  21958  ustuqtop  22050  utopsnneip  22052  prdsxmslem2  22334  isclmp  22897  iscau4  23077  caucfil  23081  iscmet3  23091  bcthlem5  23125  bcth  23126  ovolicc2lem5  23289  uniioombllem6  23356  vitali  23382  ismbf3d  23421  itg1climres  23481  itg2seq  23509  itg2monolem1  23517  itg2mono  23520  rolle  23753  dvlipcn  23757  dvivthlem1  23771  ply1divex  23896  fta1g  23927  dgrco  24031  plydivex  24052  fta1  24063  vieta1  24067  ulmcaulem  24148  ulmcau  24149  abelthlem8  24193  wilth  24797  fta  24806  dchrelbas3  24963  2sqlem6  25148  2sqlem10  25153  dchrisumlem3  25180  dchrisum  25181  dchrmusumlema  25182  dchrvmasumlema  25189  dchrisum0lema  25203  pntibndlem3  25281  pntlem3  25298  pntleml  25300  pnt3  25301  ostth2lem2  25323  ostth  25328  axcontlem1  25844  axcontlem6  25849  uspgr2wlkeq  26542  crctcshwlkn0  26713  frgrwopreglem5ALT  27186  grpoideu  27363  ubthlem3  27728  adjsym  28692  lnopunilem1  28869  elunop2  28872  lnophm  28878  cnlnadjlem5  28930  mdbr3  29156  mdbr4  29157  dmdbr3  29164  dmdbr4  29165  mddmd2  29168  fprodex01  29571  toslublem  29667  tosglblem  29669  archiabl  29752  isarchiofld  29817  qtophaus  29903  lmdvg  29999  prodindf  30085  esumcvg  30148  unelldsys  30221  ldgenpisyslem1  30226  eulerpartlemsv3  30423  eulerpartlemgvv  30438  signstfvneq0  30649  reprinfz1  30700  tgoldbachgtd  30740  bnj1185  30864  bnj1379  30901  bnj222  30953  bnj517  30955  bnj1450  31118  bnj1452  31120  bnj1463  31123  derangenlem  31153  subfacp1lem6  31167  subfacp1  31168  resconn  31228  cvmscbv  31240  untangtr  31591  dfon2lem3  31690  dfon2lem7  31694  frrlem1  31780  nosupdm  31850  nosupbnd1lem4  31857  nosupbnd2  31862  nn0prpwlem  32317  neibastop3  32357  fnemeet2  32362  phpreu  33393  poimirlem27  33436  heicant  33444  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  mbfresfi  33456  upixp  33524  sdclem2  33538  fdc  33541  mettrifi  33553  heiborlem5  33614  heiborlem10  33619  heibor  33620  bfp  33623  cdleme25cv  35646  cdleme40v  35757  mzpclval  37288  dford3lem1  37593  fnwe2lem1  37620  aomclem3  37626  aomclem4  37627  aomclem8  37631  dfac11  37632  hbtlem5  37698  ntrk2imkb  38335  ntrclsk2  38366  ntrclsk4  38370  fnchoice  39188  cncmpmax  39191  wessf1ornlem  39371  disjinfi  39380  rnmptbdd  39456  rnmptbd2  39464  rnmptbd  39471  supxrunb3  39623  unb2ltle  39642  uzubioo2  39796  mccl  39830  climsuse  39840  limsupre  39873  limsuppnfd  39934  limsuppnf  39943  limsupubuz  39945  limsupmnf  39953  limsupre2  39957  limsupmnfuz  39959  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uzlem  39967  limsupre3uz  39968  limsupreuz  39969  limsupvaluz2  39970  limsupreuzmpt  39971  climuz  39976  lmbr3  39979  limsupge  39993  liminfreuz  40035  cnrefiisp  40056  xlimmnf  40067  xlimpnf  40068  xlimmnfmpt  40069  xlimpnfmpt  40070  dfxlim2  40074  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem3  40163  stoweidlem7  40224  stoweidlem15  40232  stoweidlem35  40252  wallispilem3  40284  fourierdlem68  40391  fourierdlem71  40394  fourierdlem73  40396  fourierdlem87  40410  fourierdlem100  40423  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem109  40432  fourierdlem112  40435  etransc  40500  qndenserrnbllem  40514  dfsalgen2  40559  subsaliuncl  40576  meaiuninclem  40697  ovnsubaddlem2  40785  hoidmvlelem5  40813  hoidmvle  40814  hoiqssbllem3  40838  vonioo  40896  vonicc  40899  issmf  40937  issmfle  40954  issmfgt  40965  issmfge  40978  smfsuplem2  41018  sbgoldbm  41672  mogoldbb  41673  bgoldbtbndlem4  41696  bgoldbtbnd  41697  nn0sumshdiglem1  42415