Theorem cbvralvw 3228

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3354 with a disjoint variable condition, which does not require ax-10 2129, ax-11 2146, ax-12 2163, ax-13 2365. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2365. (Revised by Gino Giotto, 10-Jan-2024.)

Hypothesis

Ref	Expression
cbvralvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralvw	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralvw

Step	Hyp	Ref	Expression
1		eleq1w 2810	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2031	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3056	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3056	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531   ∈ wcel 2098  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-clel 2804  df-ral 3056

This theorem is referenced by:  cbvraldva  3230  cbvral2vw  3232  cbvral3vw  3234  cbvral4vw  3235  reu7  3723  disjxun  5139  reusv3i  5395  wereu2  5666  cnvpo  6280  frpomin  6335  f1mpt  7256  dfwe2  7758  tfinds  7846  frrlem1  8272  wfrlem1OLD  8309  tfrlem1  8377  tfrlem12  8390  rdglem1  8416  tz7.48lem  8442  nneneq  9211  nneneqOLD  9223  marypha1lem  9430  supub  9456  suplub  9457  ordtypecbv  9514  ordtypelem3  9517  ordtypelem9  9523  wemaplem1  9543  brwdom3  9579  ttrclss  9717  ttrclselem2  9723  tcrank  9881  infxpenc2  10019  aceq1  10114  aceq2  10116  dfac5  10125  dfac9  10133  dfac12lem3  10142  kmlem12  10158  kmlem14  10160  cofsmo  10266  infpssrlem4  10303  isfin3ds  10326  isf32lem2  10351  isf32lem11  10360  isf33lem  10363  domtriomlem  10439  axdc3  10451  zorn2lem7  10499  zorn2g  10500  fpwwe2cbv  10627  fpwwecbv  10641  pwfseq  10661  axgroth6  10825  dedekind  11381  suprleub  12184  infregelb  12202  nnsub  12260  uzwo  12899  ublbneg  12921  zsupss  12925  xrub  13297  fsuppmapnn0fiubex  13963  monoord2  14004  faclbnd4lem4  14261  bccl  14287  hashbc  14418  wrdind  14678  wrd2ind  14679  reuccatpfxs1  14703  cau3lem  15307  climmpt2  15523  caucvgrlem  15625  caurcvg2  15630  caucvgb  15632  fsum0diag2  15735  incexclem  15788  cvgrat  15835  mertenslem2  15837  mertens  15838  sqrt2irr  16199  gcdcllem1  16447  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  prmind2  16629  prmpwdvds  16846  prmreclem5  16862  prmreclem6  16863  vdwlem7  16929  vdwlem10  16932  vdwlem13  16935  vdwnn  16940  ramcl  16971  isacs2  17606  catpropd  17662  grpinvalem  18606  grpinva  18607  gsumvalx  18609  mndind  18753  issubg4  19072  isnsg2  19083  elnmz  19090  gsmsymgreqlem2  19351  psgnunilem5  19414  psgnunilem3  19416  efgsdm  19650  gsummptnn0fzfv  19907  pgpfac1lem5  20001  pgpfac1  20002  pgpfac  20006  ablfaclem3  20009  lbsextg  21013  evlslem2  21984  mpfind  22012  cply1mul  22170  mdetuni0  22478  m2cpminvid2lem  22611  mp2pm2mplem4  22666  chcoeffeqlem  22742  cayhamlem3  22744  elcls3  22942  isclo2  22947  neiptopnei  22991  tgcn  23111  subbascn  23113  txcmplem2  23501  kqfvima  23589  kqt0lem  23595  isr0  23596  r0cld  23597  regr1lem2  23599  fbun  23699  flftg  23855  fclsbas  23880  alexsubALTlem2  23907  alexsubALTlem4  23909  ptcmplem4  23914  tsmsxplem1  24012  tsmsxp  24014  ustuqtop  24106  utopsnneip  24108  prdsxmslem2  24393  isclmp  24979  iscau4  25162  caucfil  25166  iscmet3  25176  bcthlem5  25211  bcth  25212  ovolicc2lem5  25405  uniioombllem6  25472  vitali  25497  ismbf3d  25538  itg1climres  25599  itg2seq  25627  itg2monolem1  25635  itg2mono  25638  rolle  25877  dvlipcn  25882  dvivthlem1  25896  ply1divex  26027  fta1g  26059  dgrco  26165  plydivex  26187  fta1  26198  vieta1  26202  ulmcaulem  26285  ulmcau  26286  abelthlem8  26331  wilth  26958  fta  26967  fsumdvdsmul  27082  dchrelbas3  27126  2sqlem6  27311  2sqlem10  27316  dchrisumlem3  27379  dchrisum  27380  dchrmusumlema  27381  dchrvmasumlema  27388  dchrisum0lema  27402  pntibndlem3  27480  pntlem3  27497  pntleml  27499  pnt3  27500  ostth2lem2  27522  ostth  27527  nosupcbv  27590  nosupdm  27592  nosupbnd1lem4  27599  nosupbnd2  27604  noinfcbv  27605  noinfdm  27607  noinfres  27610  noinfbnd1lem1  27611  noinfbnd2  27619  madebdayim  27769  madebday  27781  cofss  27805  coiniss  27806  precsexlem9  28068  axcontlem1  28730  axcontlem6  28735  uspgr2wlkeq  29412  crctcshwlkn0  29584  frgrwopreglem5ALT  30084  grpoideu  30271  ubthlem3  30634  adjsym  31595  lnopunilem1  31772  elunop2  31775  lnophm  31781  cnlnadjlem5  31833  mdbr3  32059  mdbr4  32060  dmdbr3  32067  dmdbr4  32068  mddmd2  32071  fprodex01  32536  wrdt2ind  32622  toslublem  32647  tosglblem  32649  archiabl  32850  isarchiofld  32938  fedgmul  33234  qtophaus  33346  lmdvg  33463  prodindf  33551  esumcvg  33614  unelldsys  33686  ldgenpisyslem1  33691  eulerpartlemsv3  33890  eulerpartlemgvv  33905  signstfvneq0  34113  reprinfz1  34163  tgoldbachgtd  34203  bnj1185  34333  bnj222  34423  bnj517  34425  bnj1452  34592  bnj1463  34595  derangenlem  34690  subfacp1lem6  34704  subfacp1  34705  resconn  34765  cvmscbv  34777  sat1el2xp  34898  untangtr  35217  dfon2lem3  35290  dfon2lem7  35294  nn0prpwlem  35715  neibastop3  35755  fnemeet2  35760  fvineqsnf1  36798  fvineqsneu  36799  pibt2  36805  phpreu  36985  poimirlem27  37028  heicant  37036  mblfinlem2  37039  ovoliunnfl  37043  voliunnfl  37045  mbfresfi  37047  upixp  37110  sdclem2  37123  fdc  37126  mettrifi  37138  heiborlem5  37196  heiborlem10  37201  heibor  37202  bfp  37205  disjressuc2  37771  cdleme25cv  39742  cdleme40v  39853  aks4d1p7  41464  aks6d1c1p3  41487  aks6d1c1p4  41488  fsuppind  41719  mzpclval  42041  dford3lem1  42343  fnwe2lem1  42370  aomclem3  42376  aomclem4  42377  aomclem8  42381  dfac11  42382  hbtlem5  42448  nadd1suc  42718  ntrk2imkb  43364  ntrclsk2  43395  ntrclsk4  43399  fnchoice  44289  cncmpmax  44292  wessf1ornlem  44456  disjinfi  44463  rnmptbdd  44521  rnmptbd2  44525  rnmptbd  44532  supxrunb3  44681  unb2ltle  44697  monoord2xrv  44766  uzubioo2  44854  mccl  44886  climsuse  44896  limsupre  44929  limsuppnf  44999  limsupubuz  45001  limsupmnf  45009  limsupre2  45013  limsupmnfuz  45015  limsupre2mpt  45018  limsupre3  45021  limsupre3mpt  45022  limsupre3uzlem  45023  limsupre3uz  45024  limsupreuz  45025  limsupvaluz2  45026  limsupreuzmpt  45027  climuz  45032  lmbr3  45035  limsupge  45049  liminflelimsup  45064  liminfreuz  45091  xlimpnfxnegmnf  45102  cnrefiisp  45118  xlimmnf  45129  xlimpnf  45130  xlimmnfmpt  45131  xlimpnfmpt  45132  dfxlim2  45136  dvbdfbdioolem2  45217  dvbdfbdioo  45218  ioodvbdlimc1lem1  45219  ioodvbdlimc1lem2  45220  ioodvbdlimc2lem  45222  dvnprodlem3  45236  stoweidlem7  45295  stoweidlem15  45303  stoweidlem35  45323  wallispilem3  45355  fourierdlem68  45462  fourierdlem71  45465  fourierdlem73  45467  fourierdlem87  45481  fourierdlem100  45494  fourierdlem103  45497  fourierdlem104  45498  fourierdlem107  45501  fourierdlem109  45503  fourierdlem112  45506  etransc  45571  qndenserrnbllem  45582  dfsalgen2  45629  subsaliuncl  45646  meaiuninclem  45768  ovnsubaddlem2  45859  hoidmvlelem5  45887  hoidmvle  45888  hoiqssbllem3  45912  vonioo  45970  vonicc  45973  issmf  46016  issmfle  46033  issmfgt  46044  issmfge  46058  smfsuplem2  46100  2reuimp0  46394  uniimafveqt  46621  sbgoldbm  47024  mogoldbb  47025  bgoldbtbndlem4  47048  bgoldbtbnd  47049  nn0sumshdiglem1  47582  ipolub  47887  ipoglb  47890