Theorem cbvralvw 3249

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3360 with a disjoint variable condition, which does not require ax-10 2182, ax-11 2198, ax-12 2219, ax-13 2410. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2410. (Revised by GG, 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 2852	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2063	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3086	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ral 3086

This theorem is referenced by:  cbvraldva  3251  cbvral2vw  3253  cbvral3vw  3255  cbvral4vw  3256  reu7  3704  cbviinv  5008  disjxun  5111  reusv3i  5376  wereu2  5659  cnvpo  6289  frpomin  6342  f1mpt  7260  dfwe2  7773  tfinds  7856  frrlem1  8283  tfrlem1  8362  tfrlem12  8376  rdglem1  8402  tz7.48lem  8428  cbvixpv  8913  nneneq  9190  marypha1lem  9393  supub  9419  suplub  9420  ordtypecbv  9479  ordtypelem3  9482  ordtypelem9  9488  wemaplem1  9508  brwdom3  9544  ttrclss  9689  ttrclselem2  9695  tcrank  9856  infxpenc2  10006  aceq1  10101  aceq2  10103  dfac5  10112  dfac9  10120  dfac12lem3  10129  kmlem12  10145  kmlem14  10147  cofsmo  10253  infpssrlem4  10290  isfin3ds  10313  isf32lem2  10338  isf32lem11  10347  isf33lem  10350  domtriomlem  10426  axdc3  10438  zorn2lem7  10486  zorn2g  10487  fpwwe2cbv  10615  fpwwecbv  10629  pwfseq  10649  axgroth6  10813  dedekind  11373  suprleub  12181  infregelb  12199  nnsub  12280  uzwo  12935  ublbneg  12957  zsupss  12961  xrub  13338  fsuppmapnn0fiubex  14028  monoord2  14069  faclbnd4lem4  14332  bccl  14358  hashbc  14490  wrdind  14759  wrd2ind  14760  reuccatpfxs1  14784  cau3lem  15406  climmpt2  15624  caucvgrlem  15724  caurcvg2  15729  caucvgb  15731  fsum0diag2  15834  incexclem  15890  cvgrat  15937  mertenslem2  15939  mertens  15940  sqrt2irr  16305  gcdcllem1  16557  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  prmind2  16743  prmpwdvds  16964  prmreclem5  16980  prmreclem6  16981  vdwlem7  17047  vdwlem10  17050  vdwlem13  17053  vdwnn  17058  ramcl  17089  isacs2  17709  catpropd  17765  chnind  18677  chnub  18678  grpinvalem  18731  grpinva  18732  gsumvalx  18734  mndind  18887  issubg4  19212  isnsg2  19222  elnmz  19229  gsmsymgreqlem2  19501  psgnunilem5  19564  psgnunilem3  19566  efgsdm  19800  gsummptnn0fzfv  20057  pgpfac1lem5  20151  pgpfac1  20152  pgpfac  20156  ablfaclem3  20159  lbsextg  21264  evlslem2  22199  mpfind  22235  cply1mul  22425  mdetuni0  22747  m2cpminvid2lem  22880  mp2pm2mplem4  22935  chcoeffeqlem  23011  cayhamlem3  23013  elcls3  23209  isclo2  23214  neiptopnei  23258  tgcn  23378  subbascn  23380  txcmplem2  23768  kqfvima  23856  kqt0lem  23862  isr0  23863  r0cld  23864  regr1lem2  23866  fbun  23966  flftg  24122  fclsbas  24147  alexsubALTlem2  24174  alexsubALTlem4  24176  ptcmplem4  24181  tsmsxplem1  24279  tsmsxp  24281  ustuqtop  24372  utopsnneip  24374  prdsxmslem2  24655  isclmp  25225  iscau4  25407  caucfil  25411  iscmet3  25421  bcthlem5  25456  bcth  25457  ovolicc2lem5  25649  uniioombllem6  25716  vitali  25741  ismbf3d  25782  itg1climres  25842  itg2seq  25870  itg2monolem1  25878  itg2mono  25881  rolle  26118  dvlipcn  26122  dvivthlem1  26136  ply1divex  26263  fta1g  26296  dgrco  26401  plydivex  26427  fta1  26438  vieta1  26442  ulmcaulem  26523  ulmcau  26524  abelthlem8  26568  wilth  27201  fta  27210  fsumdvdsmul  27325  dchrelbas3  27368  2sqlem6  27553  2sqlem10  27558  dchrisumlem3  27621  dchrisum  27622  dchrmusumlema  27623  dchrvmasumlema  27630  dchrisum0lema  27644  pntibndlem3  27722  pntlem3  27739  pntleml  27741  pnt3  27742  ostth2lem2  27764  ostth  27769  nosupcbv  27832  nosupdm  27834  nosupbnd1lem4  27841  nosupbnd2  27846  noinfcbv  27847  noinfdm  27849  noinfres  27852  noinfbnd1lem1  27853  noinfbnd2  27861  madebdayim  28047  madebday  28059  cofss  28089  coiniss  28090  cutminmax  28095  precsexlem9  28374  onsfi  28515  n0subs  28522  bdayfinbndcbv  28625  bdayfinbndlem2  28627  z12zsodd  28641  axcontlem1  29255  axcontlem6  29260  uspgr2wlkeq  29936  crctcshwlkn0  30111  frgrwopreglem5ALT  30614  grpoideu  30802  ubthlem3  31165  adjsym  32126  lnopunilem1  32303  elunop2  32306  lnophm  32312  cnlnadjlem5  32364  mdbr3  32590  mdbr4  32591  dmdbr3  32598  dmdbr4  32599  mddmd2  32602  fprodex01  33110  prodindf  33123  wrdt2ind  33214  toslublem  33233  tosglblem  33235  archiabl  33459  isarchiofld  33460  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem4  33506  elrgspnsubrunlem2  33509  1arithidom  33772  1arithufdlem3  33781  vietadeg1  33913  vieta  33915  fedgmul  33966  fldextrspunlsplem  34008  constrconj  34080  qtophaus  34171  lmdvg  34288  esumcvg  34421  unelldsys  34493  ldgenpisyslem1  34498  eulerpartlemsv3  34696  eulerpartlemgvv  34711  signstfvneq0  34904  reprinfz1  34954  tgoldbachgtd  34994  bnj1185  35126  bnj222  35216  bnj517  35218  bnj1452  35385  bnj1463  35388  derangenlem  35596  subfacp1lem6  35610  subfacp1  35611  resconn  35671  cvmscbv  35683  sat1el2xp  35804  untangtr  36139  dfon2lem3  36208  dfon2lem7  36212  nn0prpwlem  36756  neibastop3  36796  fnemeet2  36801  weiunlem  36897  mh-infprim2bi  36981  mh-infprim3bi  36982  fvineqsnf1  37978  fvineqsneu  37979  pibt2  37985  phpreu  38177  poimirlem27  38220  heicant  38228  mblfinlem2  38231  ovoliunnfl  38235  voliunnfl  38237  mbfresfi  38239  upixp  38302  sdclem2  38315  fdc  38318  mettrifi  38330  heiborlem5  38388  heiborlem10  38393  heibor  38394  bfp  38397  disjressuc2  38984  cdleme25cv  41056  cdleme40v  41167  aks4d1p7  42774  aks6d1c1p3  42801  aks6d1c1p4  42802  supinf  42934  fsuppind  43248  mzpclval  43382  dford3lem1  43679  fnwe2lem1  43703  aomclem3  43709  aomclem4  43710  aomclem8  43714  dfac11  43715  hbtlem5  43781  nadd1suc  44045  ntrk2imkb  44689  ntrclsk2  44720  ntrclsk4  44724  fnchoice  45675  cncmpmax  45678  wessf1ornlem  45829  disjinfi  45836  rnmptbdd  45886  rnmptbd2  45890  rnmptbd  45897  supxrunb3  46040  unb2ltle  46055  monoord2xrv  46123  uzubioo2  46209  mccl  46240  climsuse  46250  limsupre  46281  limsuppnf  46351  limsupubuz  46353  limsupmnf  46361  limsupre2  46365  limsupmnfuz  46367  limsupre2mpt  46370  limsupre3  46373  limsupre3mpt  46374  limsupre3uzlem  46375  limsupre3uz  46376  limsupreuz  46377  limsupvaluz2  46378  limsupreuzmpt  46379  climuz  46384  lmbr3  46387  limsupge  46401  liminflelimsup  46416  liminfreuz  46443  xlimpnfxnegmnf  46454  cnrefiisp  46470  xlimmnf  46481  xlimpnf  46482  xlimmnfmpt  46483  xlimpnfmpt  46484  dfxlim2  46488  dvbdfbdioolem2  46569  dvbdfbdioo  46570  ioodvbdlimc1lem1  46571  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnprodlem3  46588  stoweidlem7  46647  stoweidlem15  46655  stoweidlem35  46675  wallispilem3  46707  fourierdlem68  46814  fourierdlem71  46817  fourierdlem73  46819  fourierdlem87  46833  fourierdlem100  46846  fourierdlem103  46849  fourierdlem104  46850  fourierdlem107  46853  fourierdlem109  46855  fourierdlem112  46858  etransc  46923  qndenserrnbllem  46934  dfsalgen2  46981  subsaliuncl  46998  meaiuninclem  47120  ovnsubaddlem2  47211  hoidmvlelem5  47239  hoidmvle  47240  hoiqssbllem3  47264  vonioo  47322  vonicc  47325  issmf  47368  issmfle  47385  issmfgt  47396  issmfge  47410  smfsuplem2  47452  chnerlem1  47524  2reuimp0  47774  uniimafveqt  48053  sbgoldbm  48472  mogoldbb  48473  bgoldbtbndlem4  48496  bgoldbtbnd  48497  nn0sumshdiglem1  49320  ipolub  49685  ipoglb  49688