Theorem cbvralvw 3232

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3358 with a disjoint variable condition, which does not require ax-10 2135, ax-11 2152, ax-12 2169, ax-13 2369. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2369. (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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 343	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2037	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3060	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3060	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2104  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-clel 2808  df-ral 3060

This theorem is referenced by:  cbvraldva  3234  cbvral2vw  3236  cbvral3vw  3238  cbvral4vw  3239  reu7  3727  disjxun  5145  reusv3i  5401  wereu2  5672  cnvpo  6285  frpomin  6340  f1mpt  7262  dfwe2  7763  tfinds  7851  frrlem1  8273  wfrlem1OLD  8310  tfrlem1  8378  tfrlem12  8391  rdglem1  8417  tz7.48lem  8443  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  13295  fsuppmapnn0fiubex  13961  monoord2  14003  faclbnd4lem4  14260  bccl  14286  hashbc  14416  wrdind  14676  wrd2ind  14677  reuccatpfxs1  14701  cau3lem  15305  climmpt2  15521  caucvgrlem  15623  caurcvg2  15628  caucvgb  15630  fsum0diag2  15733  incexclem  15786  cvgrat  15833  mertenslem2  15835  mertens  15836  sqrt2irr  16196  gcdcllem1  16444  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  prmind2  16626  prmpwdvds  16841  prmreclem5  16857  prmreclem6  16858  vdwlem7  16924  vdwlem10  16927  vdwlem13  16930  vdwnn  16935  ramcl  16966  isacs2  17601  catpropd  17657  grprinvlem  18598  grpinva  18599  gsumvalx  18601  mndind  18745  issubg4  19061  isnsg2  19072  elnmz  19079  gsmsymgreqlem2  19340  psgnunilem5  19403  psgnunilem3  19405  efgsdm  19639  gsummptnn0fzfv  19896  pgpfac1lem5  19990  pgpfac1  19991  pgpfac  19995  ablfaclem3  19998  lbsextg  20920  evlslem2  21861  mpfind  21889  cply1mul  22038  mdetuni0  22343  m2cpminvid2lem  22476  mp2pm2mplem4  22531  chcoeffeqlem  22607  cayhamlem3  22609  elcls3  22807  isclo2  22812  neiptopnei  22856  tgcn  22976  subbascn  22978  txcmplem2  23366  kqfvima  23454  kqt0lem  23460  isr0  23461  r0cld  23462  regr1lem2  23464  fbun  23564  flftg  23720  fclsbas  23745  alexsubALTlem2  23772  alexsubALTlem4  23774  ptcmplem4  23779  tsmsxplem1  23877  tsmsxp  23879  ustuqtop  23971  utopsnneip  23973  prdsxmslem2  24258  isclmp  24844  iscau4  25027  caucfil  25031  iscmet3  25041  bcthlem5  25076  bcth  25077  ovolicc2lem5  25270  uniioombllem6  25337  vitali  25362  ismbf3d  25403  itg1climres  25464  itg2seq  25492  itg2monolem1  25500  itg2mono  25503  rolle  25742  dvlipcn  25746  dvivthlem1  25760  ply1divex  25889  fta1g  25920  dgrco  26025  plydivex  26046  fta1  26057  vieta1  26061  ulmcaulem  26142  ulmcau  26143  abelthlem8  26187  wilth  26811  fta  26820  dchrelbas3  26977  2sqlem6  27162  2sqlem10  27167  dchrisumlem3  27230  dchrisum  27231  dchrmusumlema  27232  dchrvmasumlema  27239  dchrisum0lema  27253  pntibndlem3  27331  pntlem3  27348  pntleml  27350  pnt3  27351  ostth2lem2  27373  ostth  27378  nosupcbv  27441  nosupdm  27443  nosupbnd1lem4  27450  nosupbnd2  27455  noinfcbv  27456  noinfdm  27458  noinfres  27461  noinfbnd1lem1  27462  noinfbnd2  27470  madebdayim  27619  madebday  27631  cofss  27655  coiniss  27656  precsexlem9  27900  axcontlem1  28489  axcontlem6  28494  uspgr2wlkeq  29170  crctcshwlkn0  29342  frgrwopreglem5ALT  29842  grpoideu  30029  ubthlem3  30392  adjsym  31353  lnopunilem1  31530  elunop2  31533  lnophm  31539  cnlnadjlem5  31591  mdbr3  31817  mdbr4  31818  dmdbr3  31825  dmdbr4  31826  mddmd2  31829  fprodex01  32298  wrdt2ind  32384  toslublem  32409  tosglblem  32411  archiabl  32614  isarchiofld  32705  fedgmul  33004  qtophaus  33114  lmdvg  33231  prodindf  33319  esumcvg  33382  unelldsys  33454  ldgenpisyslem1  33459  eulerpartlemsv3  33658  eulerpartlemgvv  33673  signstfvneq0  33881  reprinfz1  33932  tgoldbachgtd  33972  bnj1185  34102  bnj222  34192  bnj517  34194  bnj1452  34361  bnj1463  34364  derangenlem  34460  subfacp1lem6  34474  subfacp1  34475  resconn  34535  cvmscbv  34547  sat1el2xp  34668  untangtr  34987  dfon2lem3  35061  dfon2lem7  35065  nn0prpwlem  35510  neibastop3  35550  fnemeet2  35555  fvineqsnf1  36594  fvineqsneu  36595  pibt2  36601  phpreu  36775  poimirlem27  36818  heicant  36826  mblfinlem2  36829  ovoliunnfl  36833  voliunnfl  36835  mbfresfi  36837  upixp  36900  sdclem2  36913  fdc  36916  mettrifi  36928  heiborlem5  36986  heiborlem10  36991  heibor  36992  bfp  36995  disjressuc2  37561  cdleme25cv  39532  cdleme40v  39643  aks4d1p7  41254  fsuppind  41464  mzpclval  41765  dford3lem1  42067  fnwe2lem1  42094  aomclem3  42100  aomclem4  42101  aomclem8  42105  dfac11  42106  hbtlem5  42172  nadd1suc  42444  ntrk2imkb  43090  ntrclsk2  43121  ntrclsk4  43125  fnchoice  44015  cncmpmax  44018  wessf1ornlem  44182  disjinfi  44189  rnmptbdd  44247  rnmptbd2  44251  rnmptbd  44258  supxrunb3  44407  unb2ltle  44423  monoord2xrv  44492  uzubioo2  44580  mccl  44612  climsuse  44622  limsupre  44655  limsuppnf  44725  limsupubuz  44727  limsupmnf  44735  limsupre2  44739  limsupmnfuz  44741  limsupre2mpt  44744  limsupre3  44747  limsupre3mpt  44748  limsupre3uzlem  44749  limsupre3uz  44750  limsupreuz  44751  limsupvaluz2  44752  limsupreuzmpt  44753  climuz  44758  lmbr3  44761  limsupge  44775  liminflelimsup  44790  liminfreuz  44817  xlimpnfxnegmnf  44828  cnrefiisp  44844  xlimmnf  44855  xlimpnf  44856  xlimmnfmpt  44857  xlimpnfmpt  44858  dfxlim2  44862  dvbdfbdioolem2  44943  dvbdfbdioo  44944  ioodvbdlimc1lem1  44945  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnprodlem3  44962  stoweidlem7  45021  stoweidlem15  45029  stoweidlem35  45049  wallispilem3  45081  fourierdlem68  45188  fourierdlem71  45191  fourierdlem73  45193  fourierdlem87  45207  fourierdlem100  45220  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  fourierdlem109  45229  fourierdlem112  45232  etransc  45297  qndenserrnbllem  45308  dfsalgen2  45355  subsaliuncl  45372  meaiuninclem  45494  ovnsubaddlem2  45585  hoidmvlelem5  45613  hoidmvle  45614  hoiqssbllem3  45638  vonioo  45696  vonicc  45699  issmf  45742  issmfle  45759  issmfgt  45770  issmfge  45784  smfsuplem2  45826  2reuimp0  46120  uniimafveqt  46347  sbgoldbm  46750  mogoldbb  46751  bgoldbtbndlem4  46774  bgoldbtbnd  46775  nn0sumshdiglem1  47394  ipolub  47700  ipoglb  47703