Theorem cbvralvw 3361

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3364 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2175, ax-13 2379. (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 2834	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 348	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2043	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3075	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3075	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  ∀wral 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2830  df-ral 3075

This theorem is referenced by:  cbvral2vw  3373  cbvral3vw  3375  reu7  3646  disjxun  5030  reusv3i  5273  wereu2  5521  cnvpo  6116  f1mpt  7011  dfwe2  7495  tfinds  7573  wfrlem1  7964  tfrlem1  8022  tfrlem12  8035  rdglem1  8061  tz7.48lem  8087  nneneq  8722  marypha1lem  8930  supub  8956  suplub  8957  ordtypecbv  9014  ordtypelem3  9017  ordtypelem9  9023  wemaplem1  9043  brwdom3  9079  tcrank  9346  infxpenc2  9482  aceq1  9577  aceq2  9579  dfac5  9588  dfac9  9596  dfac12lem3  9605  kmlem12  9621  kmlem14  9623  cofsmo  9729  infpssrlem4  9766  isfin3ds  9789  isf32lem2  9814  isf32lem11  9823  isf33lem  9826  domtriomlem  9902  axdc3  9914  zorn2lem7  9962  zorn2g  9963  fpwwe2cbv  10090  fpwwecbv  10104  pwfseq  10124  axgroth6  10288  dedekind  10841  suprleub  11643  infregelb  11661  nnsub  11718  uzwo  12351  ublbneg  12373  zsupss  12377  xrub  12746  fsuppmapnn0fiubex  13409  monoord2  13451  faclbnd4lem4  13706  bccl  13732  hashbc  13861  wrdind  14131  wrd2ind  14132  reuccatpfxs1  14156  cau3lem  14762  climmpt2  14978  caucvgrlem  15077  caurcvg2  15082  caucvgb  15084  fsum0diag2  15186  incexclem  15239  cvgrat  15287  mertenslem2  15289  mertens  15290  sqrt2irr  15650  gcdcllem1  15898  lcmfunsnlem1  16033  lcmfunsnlem2lem1  16034  prmind2  16081  prmpwdvds  16295  prmreclem5  16311  prmreclem6  16312  vdwlem7  16378  vdwlem10  16381  vdwlem13  16384  vdwnn  16389  ramcl  16420  isacs2  16982  catpropd  17037  grprinvlem  17949  grprinvd  17950  gsumvalx  17952  mndind  18058  issubg4  18365  isnsg2  18375  elnmz  18382  gsmsymgreqlem2  18626  psgnunilem5  18689  psgnunilem3  18691  efgsdm  18923  gsummptnn0fzfv  19175  pgpfac1lem5  19269  pgpfac1  19270  pgpfac  19274  ablfaclem3  19277  lbsextg  20002  evlslem2  20842  mpfind  20870  cply1mul  21018  mdetuni0  21321  m2cpminvid2lem  21454  mp2pm2mplem4  21509  chcoeffeqlem  21585  cayhamlem3  21587  elcls3  21783  isclo2  21788  neiptopnei  21832  tgcn  21952  subbascn  21954  txcmplem2  22342  kqfvima  22430  kqt0lem  22436  isr0  22437  r0cld  22438  regr1lem2  22440  fbun  22540  flftg  22696  fclsbas  22721  alexsubALTlem2  22748  alexsubALTlem4  22750  ptcmplem4  22755  tsmsxplem1  22853  tsmsxp  22855  ustuqtop  22947  utopsnneip  22949  prdsxmslem2  23231  isclmp  23798  iscau4  23979  caucfil  23983  iscmet3  23993  bcthlem5  24028  bcth  24029  ovolicc2lem5  24221  uniioombllem6  24288  vitali  24313  ismbf3d  24354  itg1climres  24414  itg2seq  24442  itg2monolem1  24450  itg2mono  24453  rolle  24689  dvlipcn  24693  dvivthlem1  24707  ply1divex  24836  fta1g  24867  dgrco  24971  plydivex  24992  fta1  25003  vieta1  25007  ulmcaulem  25088  ulmcau  25089  abelthlem8  25133  wilth  25755  fta  25764  dchrelbas3  25921  2sqlem6  26106  2sqlem10  26111  dchrisumlem3  26174  dchrisum  26175  dchrmusumlema  26176  dchrvmasumlema  26183  dchrisum0lema  26197  pntibndlem3  26275  pntlem3  26292  pntleml  26294  pnt3  26295  ostth2lem2  26317  ostth  26322  axcontlem1  26857  axcontlem6  26862  uspgr2wlkeq  27534  crctcshwlkn0  27706  frgrwopreglem5ALT  28206  grpoideu  28391  ubthlem3  28754  adjsym  29715  lnopunilem1  29892  elunop2  29895  lnophm  29901  cnlnadjlem5  29953  mdbr3  30179  mdbr4  30180  dmdbr3  30187  dmdbr4  30188  mddmd2  30191  fprodex01  30663  wrdt2ind  30749  toslublem  30776  tosglblem  30778  archiabl  30978  isarchiofld  31042  fedgmul  31233  qtophaus  31307  lmdvg  31424  prodindf  31510  esumcvg  31573  unelldsys  31645  ldgenpisyslem1  31650  eulerpartlemsv3  31847  eulerpartlemgvv  31862  signstfvneq0  32070  reprinfz1  32121  tgoldbachgtd  32161  bnj1185  32293  bnj222  32383  bnj517  32385  bnj1452  32552  bnj1463  32555  derangenlem  32649  subfacp1lem6  32663  subfacp1  32664  resconn  32724  cvmscbv  32736  sat1el2xp  32857  untangtr  33171  dfon2lem3  33277  dfon2lem7  33281  frpomin  33325  frrlem1  33384  nosupcbv  33470  nosupdm  33472  nosupbnd1lem4  33479  nosupbnd2  33484  noinfcbv  33485  noinfdm  33487  noinfres  33490  noinfbnd1lem1  33491  noinfbnd2  33499  madebdayim  33627  madebday  33637  nn0prpwlem  34060  neibastop3  34100  fnemeet2  34105  fvineqsnf1  35107  fvineqsneu  35108  pibt2  35114  phpreu  35321  poimirlem27  35364  heicant  35372  mblfinlem2  35375  ovoliunnfl  35379  voliunnfl  35381  mbfresfi  35383  upixp  35447  sdclem2  35460  fdc  35463  mettrifi  35475  heiborlem5  35533  heiborlem10  35538  heibor  35539  bfp  35542  cdleme25cv  37934  cdleme40v  38045  fsuppind  39784  mzpclval  40039  dford3lem1  40340  fnwe2lem1  40367  aomclem3  40373  aomclem4  40374  aomclem8  40378  dfac11  40379  hbtlem5  40445  ntrk2imkb  41113  ntrclsk2  41144  ntrclsk4  41148  fnchoice  42031  cncmpmax  42034  wessf1ornlem  42181  disjinfi  42190  rnmptbdd  42250  rnmptbd2  42255  rnmptbd  42262  supxrunb3  42402  unb2ltle  42418  monoord2xrv  42489  uzubioo2  42572  mccl  42606  climsuse  42616  limsupre  42649  limsuppnf  42719  limsupubuz  42721  limsupmnf  42729  limsupre2  42733  limsupmnfuz  42735  limsupre2mpt  42738  limsupre3  42741  limsupre3mpt  42742  limsupre3uzlem  42743  limsupre3uz  42744  limsupreuz  42745  limsupvaluz2  42746  limsupreuzmpt  42747  climuz  42752  lmbr3  42755  limsupge  42769  liminflelimsup  42784  liminfreuz  42811  xlimpnfxnegmnf  42822  cnrefiisp  42838  xlimmnf  42849  xlimpnf  42850  xlimmnfmpt  42851  xlimpnfmpt  42852  dfxlim2  42856  dvbdfbdioolem2  42937  dvbdfbdioo  42938  ioodvbdlimc1lem1  42939  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  dvnprodlem3  42956  stoweidlem7  43015  stoweidlem15  43023  stoweidlem35  43043  wallispilem3  43075  fourierdlem68  43182  fourierdlem71  43185  fourierdlem73  43187  fourierdlem87  43201  fourierdlem100  43214  fourierdlem103  43217  fourierdlem104  43218  fourierdlem107  43221  fourierdlem109  43223  fourierdlem112  43226  etransc  43291  qndenserrnbllem  43302  dfsalgen2  43347  subsaliuncl  43364  meaiuninclem  43485  ovnsubaddlem2  43576  hoidmvlelem5  43604  hoidmvle  43605  hoiqssbllem3  43629  vonioo  43687  vonicc  43690  issmf  43728  issmfle  43745  issmfgt  43756  issmfge  43769  smfsuplem2  43809  2reuimp0  44038  uniimafveqt  44266  sbgoldbm  44669  mogoldbb  44670  bgoldbtbndlem4  44693  bgoldbtbnd  44694  nn0sumshdiglem1  45400