Theorem cbvralvw 3237

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 2141, ax-11 2157, ax-12 2177, ax-13 2377. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2377. (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 2824	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2035	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3062	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  ∀wral 3061

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 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ral 3062

This theorem is referenced by:  cbvraldva  3239  cbvral2vw  3241  cbvral3vw  3243  cbvral4vw  3244  reu7  3738  cbviinv  5041  disjxun  5141  reusv3i  5404  wereu2  5682  cnvpo  6307  frpomin  6361  f1mpt  7281  dfwe2  7794  tfinds  7881  frrlem1  8311  wfrlem1OLD  8348  tfrlem1  8416  tfrlem12  8429  rdglem1  8455  tz7.48lem  8481  cbvixpv  8955  nneneq  9246  nneneqOLD  9258  marypha1lem  9473  supub  9499  suplub  9500  ordtypecbv  9557  ordtypelem3  9560  ordtypelem9  9566  wemaplem1  9586  brwdom3  9622  ttrclss  9760  ttrclselem2  9766  tcrank  9924  infxpenc2  10062  aceq1  10157  aceq2  10159  dfac5  10169  dfac9  10177  dfac12lem3  10186  kmlem12  10202  kmlem14  10204  cofsmo  10309  infpssrlem4  10346  isfin3ds  10369  isf32lem2  10394  isf32lem11  10403  isf33lem  10406  domtriomlem  10482  axdc3  10494  zorn2lem7  10542  zorn2g  10543  fpwwe2cbv  10670  fpwwecbv  10684  pwfseq  10704  axgroth6  10868  dedekind  11424  suprleub  12234  infregelb  12252  nnsub  12310  uzwo  12953  ublbneg  12975  zsupss  12979  xrub  13354  fsuppmapnn0fiubex  14033  monoord2  14074  faclbnd4lem4  14335  bccl  14361  hashbc  14492  wrdind  14760  wrd2ind  14761  reuccatpfxs1  14785  cau3lem  15393  climmpt2  15609  caucvgrlem  15709  caurcvg2  15714  caucvgb  15716  fsum0diag2  15819  incexclem  15872  cvgrat  15919  mertenslem2  15921  mertens  15922  sqrt2irr  16285  gcdcllem1  16536  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  prmind2  16722  prmpwdvds  16942  prmreclem5  16958  prmreclem6  16959  vdwlem7  17025  vdwlem10  17028  vdwlem13  17031  vdwnn  17036  ramcl  17067  isacs2  17696  catpropd  17752  grpinvalem  18686  grpinva  18687  gsumvalx  18689  mndind  18841  issubg4  19163  isnsg2  19174  elnmz  19181  gsmsymgreqlem2  19449  psgnunilem5  19512  psgnunilem3  19514  efgsdm  19748  gsummptnn0fzfv  20005  pgpfac1lem5  20099  pgpfac1  20100  pgpfac  20104  ablfaclem3  20107  lbsextg  21164  evlslem2  22103  mpfind  22131  cply1mul  22300  mdetuni0  22627  m2cpminvid2lem  22760  mp2pm2mplem4  22815  chcoeffeqlem  22891  cayhamlem3  22893  elcls3  23091  isclo2  23096  neiptopnei  23140  tgcn  23260  subbascn  23262  txcmplem2  23650  kqfvima  23738  kqt0lem  23744  isr0  23745  r0cld  23746  regr1lem2  23748  fbun  23848  flftg  24004  fclsbas  24029  alexsubALTlem2  24056  alexsubALTlem4  24058  ptcmplem4  24063  tsmsxplem1  24161  tsmsxp  24163  ustuqtop  24255  utopsnneip  24257  prdsxmslem2  24542  isclmp  25130  iscau4  25313  caucfil  25317  iscmet3  25327  bcthlem5  25362  bcth  25363  ovolicc2lem5  25556  uniioombllem6  25623  vitali  25648  ismbf3d  25689  itg1climres  25749  itg2seq  25777  itg2monolem1  25785  itg2mono  25788  rolle  26028  dvlipcn  26033  dvivthlem1  26047  ply1divex  26176  fta1g  26209  dgrco  26315  plydivex  26339  fta1  26350  vieta1  26354  ulmcaulem  26437  ulmcau  26438  abelthlem8  26483  wilth  27114  fta  27123  fsumdvdsmul  27238  dchrelbas3  27282  2sqlem6  27467  2sqlem10  27472  dchrisumlem3  27535  dchrisum  27536  dchrmusumlema  27537  dchrvmasumlema  27544  dchrisum0lema  27558  pntibndlem3  27636  pntlem3  27653  pntleml  27655  pnt3  27656  ostth2lem2  27678  ostth  27683  nosupcbv  27747  nosupdm  27749  nosupbnd1lem4  27756  nosupbnd2  27761  noinfcbv  27762  noinfdm  27764  noinfres  27767  noinfbnd1lem1  27768  noinfbnd2  27776  madebdayim  27926  madebday  27938  cofss  27964  coiniss  27965  precsexlem9  28239  n0subs  28360  zs12bday  28424  axcontlem1  28979  axcontlem6  28984  uspgr2wlkeq  29664  crctcshwlkn0  29841  frgrwopreglem5ALT  30341  grpoideu  30528  ubthlem3  30891  adjsym  31852  lnopunilem1  32029  elunop2  32032  lnophm  32038  cnlnadjlem5  32090  mdbr3  32316  mdbr4  32317  dmdbr3  32324  dmdbr4  32325  mddmd2  32328  fprodex01  32827  prodindf  32848  wrdt2ind  32938  toslublem  32962  tosglblem  32964  chnind  33001  chnub  33002  archiabl  33205  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  isarchiofld  33347  1arithidom  33565  1arithufdlem3  33574  fedgmul  33682  fldextrspunlsplem  33723  constrconj  33786  qtophaus  33835  lmdvg  33952  esumcvg  34087  unelldsys  34159  ldgenpisyslem1  34164  eulerpartlemsv3  34363  eulerpartlemgvv  34378  signstfvneq0  34587  reprinfz1  34637  tgoldbachgtd  34677  bnj1185  34807  bnj222  34897  bnj517  34899  bnj1452  35066  bnj1463  35069  derangenlem  35176  subfacp1lem6  35190  subfacp1  35191  resconn  35251  cvmscbv  35263  sat1el2xp  35384  untangtr  35714  dfon2lem3  35786  dfon2lem7  35790  nn0prpwlem  36323  neibastop3  36363  fnemeet2  36368  weiunlem2  36464  fvineqsnf1  37411  fvineqsneu  37412  pibt2  37418  phpreu  37611  poimirlem27  37654  heicant  37662  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  mbfresfi  37673  upixp  37736  sdclem2  37749  fdc  37752  mettrifi  37764  heiborlem5  37822  heiborlem10  37827  heibor  37828  bfp  37831  disjressuc2  38389  cdleme25cv  40360  cdleme40v  40471  aks4d1p7  42084  aks6d1c1p3  42111  aks6d1c1p4  42112  supinf  42283  fsuppind  42600  mzpclval  42736  dford3lem1  43038  fnwe2lem1  43062  aomclem3  43068  aomclem4  43069  aomclem8  43073  dfac11  43074  hbtlem5  43140  nadd1suc  43405  ntrk2imkb  44050  ntrclsk2  44081  ntrclsk4  44085  fnchoice  45034  cncmpmax  45037  wessf1ornlem  45190  disjinfi  45197  rnmptbdd  45252  rnmptbd2  45256  rnmptbd  45263  supxrunb3  45410  unb2ltle  45426  monoord2xrv  45494  uzubioo2  45582  mccl  45613  climsuse  45623  limsupre  45656  limsuppnf  45726  limsupubuz  45728  limsupmnf  45736  limsupre2  45740  limsupmnfuz  45742  limsupre2mpt  45745  limsupre3  45748  limsupre3mpt  45749  limsupre3uzlem  45750  limsupre3uz  45751  limsupreuz  45752  limsupvaluz2  45753  limsupreuzmpt  45754  climuz  45759  lmbr3  45762  limsupge  45776  liminflelimsup  45791  liminfreuz  45818  xlimpnfxnegmnf  45829  cnrefiisp  45845  xlimmnf  45856  xlimpnf  45857  xlimmnfmpt  45858  xlimpnfmpt  45859  dfxlim2  45863  dvbdfbdioolem2  45944  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem3  45963  stoweidlem7  46022  stoweidlem15  46030  stoweidlem35  46050  wallispilem3  46082  fourierdlem68  46189  fourierdlem71  46192  fourierdlem73  46194  fourierdlem87  46208  fourierdlem100  46221  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem109  46230  fourierdlem112  46233  etransc  46298  qndenserrnbllem  46309  dfsalgen2  46356  subsaliuncl  46373  meaiuninclem  46495  ovnsubaddlem2  46586  hoidmvlelem5  46614  hoidmvle  46615  hoiqssbllem3  46639  vonioo  46697  vonicc  46700  issmf  46743  issmfle  46760  issmfgt  46771  issmfge  46785  smfsuplem2  46827  2reuimp0  47126  uniimafveqt  47368  sbgoldbm  47771  mogoldbb  47772  bgoldbtbndlem4  47795  bgoldbtbnd  47796  nn0sumshdiglem1  48542  ipolub  48877  ipoglb  48880