Theorem cbvralvw 3214

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3334 with a disjoint variable condition, which does not require ax-10 2146, ax-11 2162, ax-12 2184, ax-13 2376. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2376. (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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2037	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3052	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3052	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ral 3052

This theorem is referenced by:  cbvraldva  3216  cbvral2vw  3218  cbvral3vw  3220  cbvral4vw  3221  reu7  3690  cbviinv  4995  disjxun  5096  reusv3i  5349  wereu2  5621  cnvpo  6245  frpomin  6298  f1mpt  7207  dfwe2  7719  tfinds  7802  frrlem1  8228  tfrlem1  8307  tfrlem12  8320  rdglem1  8346  tz7.48lem  8372  cbvixpv  8855  nneneq  9132  marypha1lem  9338  supub  9364  suplub  9365  ordtypecbv  9424  ordtypelem3  9427  ordtypelem9  9433  wemaplem1  9453  brwdom3  9489  ttrclss  9631  ttrclselem2  9637  tcrank  9798  infxpenc2  9934  aceq1  10029  aceq2  10031  dfac5  10041  dfac9  10049  dfac12lem3  10058  kmlem12  10074  kmlem14  10076  cofsmo  10181  infpssrlem4  10218  isfin3ds  10241  isf32lem2  10266  isf32lem11  10275  isf33lem  10278  domtriomlem  10354  axdc3  10366  zorn2lem7  10414  zorn2g  10415  fpwwe2cbv  10543  fpwwecbv  10557  pwfseq  10577  axgroth6  10741  dedekind  11298  suprleub  12110  infregelb  12128  nnsub  12191  uzwo  12826  ublbneg  12848  zsupss  12852  xrub  13229  fsuppmapnn0fiubex  13917  monoord2  13958  faclbnd4lem4  14221  bccl  14247  hashbc  14378  wrdind  14647  wrd2ind  14648  reuccatpfxs1  14672  cau3lem  15280  climmpt2  15498  caucvgrlem  15598  caurcvg2  15603  caucvgb  15605  fsum0diag2  15708  incexclem  15761  cvgrat  15808  mertenslem2  15810  mertens  15811  sqrt2irr  16176  gcdcllem1  16428  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  prmind2  16614  prmpwdvds  16834  prmreclem5  16850  prmreclem6  16851  vdwlem7  16917  vdwlem10  16920  vdwlem13  16923  vdwnn  16928  ramcl  16959  isacs2  17578  catpropd  17634  chnind  18546  chnub  18547  grpinvalem  18600  grpinva  18601  gsumvalx  18603  mndind  18755  issubg4  19077  isnsg2  19087  elnmz  19094  gsmsymgreqlem2  19362  psgnunilem5  19425  psgnunilem3  19427  efgsdm  19661  gsummptnn0fzfv  19918  pgpfac1lem5  20012  pgpfac1  20013  pgpfac  20017  ablfaclem3  20020  lbsextg  21119  evlslem2  22036  mpfind  22072  cply1mul  22242  mdetuni0  22567  m2cpminvid2lem  22700  mp2pm2mplem4  22755  chcoeffeqlem  22831  cayhamlem3  22833  elcls3  23029  isclo2  23034  neiptopnei  23078  tgcn  23198  subbascn  23200  txcmplem2  23588  kqfvima  23676  kqt0lem  23682  isr0  23683  r0cld  23684  regr1lem2  23686  fbun  23786  flftg  23942  fclsbas  23967  alexsubALTlem2  23994  alexsubALTlem4  23996  ptcmplem4  24001  tsmsxplem1  24099  tsmsxp  24101  ustuqtop  24192  utopsnneip  24194  prdsxmslem2  24475  isclmp  25055  iscau4  25237  caucfil  25241  iscmet3  25251  bcthlem5  25286  bcth  25287  ovolicc2lem5  25480  uniioombllem6  25547  vitali  25572  ismbf3d  25613  itg1climres  25673  itg2seq  25701  itg2monolem1  25709  itg2mono  25712  rolle  25952  dvlipcn  25957  dvivthlem1  25971  ply1divex  26100  fta1g  26133  dgrco  26239  plydivex  26263  fta1  26274  vieta1  26278  ulmcaulem  26361  ulmcau  26362  abelthlem8  26407  wilth  27039  fta  27048  fsumdvdsmul  27163  dchrelbas3  27207  2sqlem6  27392  2sqlem10  27397  dchrisumlem3  27460  dchrisum  27461  dchrmusumlema  27462  dchrvmasumlema  27469  dchrisum0lema  27483  pntibndlem3  27561  pntlem3  27578  pntleml  27580  pnt3  27581  ostth2lem2  27603  ostth  27608  nosupcbv  27672  nosupdm  27674  nosupbnd1lem4  27681  nosupbnd2  27686  noinfcbv  27687  noinfdm  27689  noinfres  27692  noinfbnd1lem1  27693  noinfbnd2  27701  madebdayim  27886  madebday  27898  cofss  27928  coiniss  27929  cutminmax  27934  precsexlem9  28213  onsfi  28354  n0subs  28361  bdayfinbndcbv  28464  bdayfinbndlem2  28466  z12zsodd  28480  axcontlem1  29039  axcontlem6  29044  uspgr2wlkeq  29721  crctcshwlkn0  29896  frgrwopreglem5ALT  30399  grpoideu  30586  ubthlem3  30949  adjsym  31910  lnopunilem1  32087  elunop2  32090  lnophm  32096  cnlnadjlem5  32148  mdbr3  32374  mdbr4  32375  dmdbr3  32382  dmdbr4  32383  mddmd2  32386  fprodex01  32908  prodindf  32946  wrdt2ind  33037  toslublem  33056  tosglblem  33058  archiabl  33282  isarchiofld  33283  elrgspnlem1  33326  elrgspnlem2  33327  elrgspnlem4  33329  elrgspnsubrunlem2  33332  1arithidom  33620  1arithufdlem3  33629  vietadeg1  33736  vieta  33738  fedgmul  33790  fldextrspunlsplem  33832  constrconj  33904  qtophaus  33995  lmdvg  34112  esumcvg  34245  unelldsys  34317  ldgenpisyslem1  34322  eulerpartlemsv3  34520  eulerpartlemgvv  34535  signstfvneq0  34731  reprinfz1  34781  tgoldbachgtd  34821  bnj1185  34951  bnj222  35041  bnj517  35043  bnj1452  35210  bnj1463  35213  derangenlem  35367  subfacp1lem6  35381  subfacp1  35382  resconn  35442  cvmscbv  35454  sat1el2xp  35575  untangtr  35910  dfon2lem3  35979  dfon2lem7  35983  nn0prpwlem  36518  neibastop3  36558  fnemeet2  36563  weiunlem  36659  fvineqsnf1  37617  fvineqsneu  37618  pibt2  37624  phpreu  37807  poimirlem27  37850  heicant  37858  mblfinlem2  37861  ovoliunnfl  37865  voliunnfl  37867  mbfresfi  37869  upixp  37932  sdclem2  37945  fdc  37948  mettrifi  37960  heiborlem5  38018  heiborlem10  38023  heibor  38024  bfp  38027  disjressuc2  38609  cdleme25cv  40640  cdleme40v  40751  aks4d1p7  42359  aks6d1c1p3  42386  aks6d1c1p4  42387  supinf  42518  fsuppind  42854  mzpclval  42988  dford3lem1  43289  fnwe2lem1  43313  aomclem3  43319  aomclem4  43320  aomclem8  43324  dfac11  43325  hbtlem5  43391  nadd1suc  43655  ntrk2imkb  44299  ntrclsk2  44330  ntrclsk4  44334  fnchoice  45295  cncmpmax  45298  wessf1ornlem  45450  disjinfi  45457  rnmptbdd  45510  rnmptbd2  45514  rnmptbd  45521  supxrunb3  45664  unb2ltle  45680  monoord2xrv  45748  uzubioo2  45834  mccl  45865  climsuse  45875  limsupre  45906  limsuppnf  45976  limsupubuz  45978  limsupmnf  45986  limsupre2  45990  limsupmnfuz  45992  limsupre2mpt  45995  limsupre3  45998  limsupre3mpt  45999  limsupre3uzlem  46000  limsupre3uz  46001  limsupreuz  46002  limsupvaluz2  46003  limsupreuzmpt  46004  climuz  46009  lmbr3  46012  limsupge  46026  liminflelimsup  46041  liminfreuz  46068  xlimpnfxnegmnf  46079  cnrefiisp  46095  xlimmnf  46106  xlimpnf  46107  xlimmnfmpt  46108  xlimpnfmpt  46109  dfxlim2  46113  dvbdfbdioolem2  46194  dvbdfbdioo  46195  ioodvbdlimc1lem1  46196  ioodvbdlimc1lem2  46197  ioodvbdlimc2lem  46199  dvnprodlem3  46213  stoweidlem7  46272  stoweidlem15  46280  stoweidlem35  46300  wallispilem3  46332  fourierdlem68  46439  fourierdlem71  46442  fourierdlem73  46444  fourierdlem87  46458  fourierdlem100  46471  fourierdlem103  46474  fourierdlem104  46475  fourierdlem107  46478  fourierdlem109  46480  fourierdlem112  46483  etransc  46548  qndenserrnbllem  46559  dfsalgen2  46606  subsaliuncl  46623  meaiuninclem  46745  ovnsubaddlem2  46836  hoidmvlelem5  46864  hoidmvle  46865  hoiqssbllem3  46889  vonioo  46947  vonicc  46950  issmf  46993  issmfle  47010  issmfgt  47021  issmfge  47035  smfsuplem2  47077  chnerlem1  47147  2reuimp0  47381  uniimafveqt  47648  sbgoldbm  48051  mogoldbb  48052  bgoldbtbndlem4  48075  bgoldbtbnd  48076  nn0sumshdiglem1  48888  ipolub  49254  ipoglb  49257