Theorem cbvralvw 3384

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3389 with a disjoint variable condition, which does not require ax-10 2138, ax-11 2155, ax-12 2172, ax-13 2373. (Contributed by NM, 28-Jan-1997.) (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 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2040	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3070	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2817  df-ral 3070

This theorem is referenced by:  cbvral2vw  3397  cbvral3vw  3399  reu7  3668  disjxun  5073  reusv3i  5328  wereu2  5587  cnvpo  6194  frpomin  6247  f1mpt  7143  dfwe2  7633  tfinds  7715  frrlem1  8111  wfrlem1OLD  8148  tfrlem1  8216  tfrlem12  8229  rdglem1  8255  tz7.48lem  8281  nneneq  9001  nneneqOLD  9013  marypha1lem  9201  supub  9227  suplub  9228  ordtypecbv  9285  ordtypelem3  9288  ordtypelem9  9294  wemaplem1  9314  brwdom3  9350  ttrclss  9487  ttrclselem2  9493  tcrank  9651  infxpenc2  9787  aceq1  9882  aceq2  9884  dfac5  9893  dfac9  9901  dfac12lem3  9910  kmlem12  9926  kmlem14  9928  cofsmo  10034  infpssrlem4  10071  isfin3ds  10094  isf32lem2  10119  isf32lem11  10128  isf33lem  10131  domtriomlem  10207  axdc3  10219  zorn2lem7  10267  zorn2g  10268  fpwwe2cbv  10395  fpwwecbv  10409  pwfseq  10429  axgroth6  10593  dedekind  11147  suprleub  11950  infregelb  11968  nnsub  12026  uzwo  12660  ublbneg  12682  zsupss  12686  xrub  13055  fsuppmapnn0fiubex  13721  monoord2  13763  faclbnd4lem4  14019  bccl  14045  hashbc  14174  wrdind  14444  wrd2ind  14445  reuccatpfxs1  14469  cau3lem  15075  climmpt2  15291  caucvgrlem  15393  caurcvg2  15398  caucvgb  15400  fsum0diag2  15504  incexclem  15557  cvgrat  15604  mertenslem2  15606  mertens  15607  sqrt2irr  15967  gcdcllem1  16215  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  prmind2  16399  prmpwdvds  16614  prmreclem5  16630  prmreclem6  16631  vdwlem7  16697  vdwlem10  16700  vdwlem13  16703  vdwnn  16708  ramcl  16739  isacs2  17371  catpropd  17427  grprinvlem  18366  grprinvd  18367  gsumvalx  18369  mndind  18475  issubg4  18783  isnsg2  18793  elnmz  18800  gsmsymgreqlem2  19048  psgnunilem5  19111  psgnunilem3  19113  efgsdm  19345  gsummptnn0fzfv  19597  pgpfac1lem5  19691  pgpfac1  19692  pgpfac  19696  ablfaclem3  19699  lbsextg  20433  evlslem2  21298  mpfind  21326  cply1mul  21474  mdetuni0  21779  m2cpminvid2lem  21912  mp2pm2mplem4  21967  chcoeffeqlem  22043  cayhamlem3  22045  elcls3  22243  isclo2  22248  neiptopnei  22292  tgcn  22412  subbascn  22414  txcmplem2  22802  kqfvima  22890  kqt0lem  22896  isr0  22897  r0cld  22898  regr1lem2  22900  fbun  23000  flftg  23156  fclsbas  23181  alexsubALTlem2  23208  alexsubALTlem4  23210  ptcmplem4  23215  tsmsxplem1  23313  tsmsxp  23315  ustuqtop  23407  utopsnneip  23409  prdsxmslem2  23694  isclmp  24269  iscau4  24452  caucfil  24456  iscmet3  24466  bcthlem5  24501  bcth  24502  ovolicc2lem5  24694  uniioombllem6  24761  vitali  24786  ismbf3d  24827  itg1climres  24888  itg2seq  24916  itg2monolem1  24924  itg2mono  24927  rolle  25163  dvlipcn  25167  dvivthlem1  25181  ply1divex  25310  fta1g  25341  dgrco  25445  plydivex  25466  fta1  25477  vieta1  25481  ulmcaulem  25562  ulmcau  25563  abelthlem8  25607  wilth  26229  fta  26238  dchrelbas3  26395  2sqlem6  26580  2sqlem10  26585  dchrisumlem3  26648  dchrisum  26649  dchrmusumlema  26650  dchrvmasumlema  26657  dchrisum0lema  26671  pntibndlem3  26749  pntlem3  26766  pntleml  26768  pnt3  26769  ostth2lem2  26791  ostth  26796  axcontlem1  27341  axcontlem6  27346  uspgr2wlkeq  28022  crctcshwlkn0  28195  frgrwopreglem5ALT  28695  grpoideu  28880  ubthlem3  29243  adjsym  30204  lnopunilem1  30381  elunop2  30384  lnophm  30390  cnlnadjlem5  30442  mdbr3  30668  mdbr4  30669  dmdbr3  30676  dmdbr4  30677  mddmd2  30680  fprodex01  31148  wrdt2ind  31234  toslublem  31259  tosglblem  31261  archiabl  31461  isarchiofld  31525  fedgmul  31721  qtophaus  31795  lmdvg  31912  prodindf  32000  esumcvg  32063  unelldsys  32135  ldgenpisyslem1  32140  eulerpartlemsv3  32337  eulerpartlemgvv  32352  signstfvneq0  32560  reprinfz1  32611  tgoldbachgtd  32651  bnj1185  32782  bnj222  32872  bnj517  32874  bnj1452  33041  bnj1463  33044  derangenlem  33142  subfacp1lem6  33156  subfacp1  33157  resconn  33217  cvmscbv  33229  sat1el2xp  33350  untangtr  33664  dfon2lem3  33770  dfon2lem7  33774  nosupcbv  33914  nosupdm  33916  nosupbnd1lem4  33923  nosupbnd2  33928  noinfcbv  33929  noinfdm  33931  noinfres  33934  noinfbnd1lem1  33935  noinfbnd2  33943  madebdayim  34079  madebday  34089  nn0prpwlem  34520  neibastop3  34560  fnemeet2  34565  fvineqsnf1  35590  fvineqsneu  35591  pibt2  35597  phpreu  35770  poimirlem27  35813  heicant  35821  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  mbfresfi  35832  upixp  35896  sdclem2  35909  fdc  35912  mettrifi  35924  heiborlem5  35982  heiborlem10  35987  heibor  35988  bfp  35991  cdleme25cv  38379  cdleme40v  38490  aks4d1p7  40098  fsuppind  40286  mzpclval  40554  dford3lem1  40855  fnwe2lem1  40882  aomclem3  40888  aomclem4  40889  aomclem8  40893  dfac11  40894  hbtlem5  40960  ntrk2imkb  41654  ntrclsk2  41685  ntrclsk4  41689  fnchoice  42579  cncmpmax  42582  wessf1ornlem  42729  disjinfi  42738  rnmptbdd  42797  rnmptbd2  42802  rnmptbd  42809  supxrunb3  42946  unb2ltle  42962  monoord2xrv  43031  uzubioo2  43114  mccl  43146  climsuse  43156  limsupre  43189  limsuppnf  43259  limsupubuz  43261  limsupmnf  43269  limsupre2  43273  limsupmnfuz  43275  limsupre2mpt  43278  limsupre3  43281  limsupre3mpt  43282  limsupre3uzlem  43283  limsupre3uz  43284  limsupreuz  43285  limsupvaluz2  43286  limsupreuzmpt  43287  climuz  43292  lmbr3  43295  limsupge  43309  liminflelimsup  43324  liminfreuz  43351  xlimpnfxnegmnf  43362  cnrefiisp  43378  xlimmnf  43389  xlimpnf  43390  xlimmnfmpt  43391  xlimpnfmpt  43392  dfxlim2  43396  dvbdfbdioolem2  43477  dvbdfbdioo  43478  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem3  43496  stoweidlem7  43555  stoweidlem15  43563  stoweidlem35  43583  wallispilem3  43615  fourierdlem68  43722  fourierdlem71  43725  fourierdlem73  43727  fourierdlem87  43741  fourierdlem100  43754  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem109  43763  fourierdlem112  43766  etransc  43831  qndenserrnbllem  43842  dfsalgen2  43887  subsaliuncl  43904  meaiuninclem  44025  ovnsubaddlem2  44116  hoidmvlelem5  44144  hoidmvle  44145  hoiqssbllem3  44169  vonioo  44227  vonicc  44230  issmf  44273  issmfle  44290  issmfgt  44301  issmfge  44315  smfsuplem2  44356  2reuimp0  44617  uniimafveqt  44844  sbgoldbm  45247  mogoldbb  45248  bgoldbtbndlem4  45271  bgoldbtbnd  45272  nn0sumshdiglem1  45978  ipolub  46285  ipoglb  46288