Theorem cbvralvw 3213

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

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 2008  ax-8 2111

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

This theorem is referenced by:  cbvraldva  3215  cbvral2vw  3217  cbvral3vw  3219  cbvral4vw  3220  reu7  3700  cbviinv  5000  disjxun  5100  reusv3i  5354  wereu2  5628  cnvpo  6248  frpomin  6301  f1mpt  7218  dfwe2  7730  tfinds  7816  frrlem1  8242  tfrlem1  8321  tfrlem12  8334  rdglem1  8360  tz7.48lem  8386  cbvixpv  8865  nneneq  9147  marypha1lem  9360  supub  9386  suplub  9387  ordtypecbv  9446  ordtypelem3  9449  ordtypelem9  9455  wemaplem1  9475  brwdom3  9511  ttrclss  9649  ttrclselem2  9655  tcrank  9813  infxpenc2  9951  aceq1  10046  aceq2  10048  dfac5  10058  dfac9  10066  dfac12lem3  10075  kmlem12  10091  kmlem14  10093  cofsmo  10198  infpssrlem4  10235  isfin3ds  10258  isf32lem2  10283  isf32lem11  10292  isf33lem  10295  domtriomlem  10371  axdc3  10383  zorn2lem7  10431  zorn2g  10432  fpwwe2cbv  10559  fpwwecbv  10573  pwfseq  10593  axgroth6  10757  dedekind  11313  suprleub  12125  infregelb  12143  nnsub  12206  uzwo  12846  ublbneg  12868  zsupss  12872  xrub  13248  fsuppmapnn0fiubex  13933  monoord2  13974  faclbnd4lem4  14237  bccl  14263  hashbc  14394  wrdind  14663  wrd2ind  14664  reuccatpfxs1  14688  cau3lem  15297  climmpt2  15515  caucvgrlem  15615  caurcvg2  15620  caucvgb  15622  fsum0diag2  15725  incexclem  15778  cvgrat  15825  mertenslem2  15827  mertens  15828  sqrt2irr  16193  gcdcllem1  16445  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  prmind2  16631  prmpwdvds  16851  prmreclem5  16867  prmreclem6  16868  vdwlem7  16934  vdwlem10  16937  vdwlem13  16940  vdwnn  16945  ramcl  16976  isacs2  17594  catpropd  17650  grpinvalem  18582  grpinva  18583  gsumvalx  18585  mndind  18737  issubg4  19059  isnsg2  19070  elnmz  19077  gsmsymgreqlem2  19345  psgnunilem5  19408  psgnunilem3  19410  efgsdm  19644  gsummptnn0fzfv  19901  pgpfac1lem5  19995  pgpfac1  19996  pgpfac  20000  ablfaclem3  20003  lbsextg  21104  evlslem2  22019  mpfind  22047  cply1mul  22216  mdetuni0  22541  m2cpminvid2lem  22674  mp2pm2mplem4  22729  chcoeffeqlem  22805  cayhamlem3  22807  elcls3  23003  isclo2  23008  neiptopnei  23052  tgcn  23172  subbascn  23174  txcmplem2  23562  kqfvima  23650  kqt0lem  23656  isr0  23657  r0cld  23658  regr1lem2  23660  fbun  23760  flftg  23916  fclsbas  23941  alexsubALTlem2  23968  alexsubALTlem4  23970  ptcmplem4  23975  tsmsxplem1  24073  tsmsxp  24075  ustuqtop  24167  utopsnneip  24169  prdsxmslem2  24450  isclmp  25030  iscau4  25212  caucfil  25216  iscmet3  25226  bcthlem5  25261  bcth  25262  ovolicc2lem5  25455  uniioombllem6  25522  vitali  25547  ismbf3d  25588  itg1climres  25648  itg2seq  25676  itg2monolem1  25684  itg2mono  25687  rolle  25927  dvlipcn  25932  dvivthlem1  25946  ply1divex  26075  fta1g  26108  dgrco  26214  plydivex  26238  fta1  26249  vieta1  26253  ulmcaulem  26336  ulmcau  26337  abelthlem8  26382  wilth  27014  fta  27023  fsumdvdsmul  27138  dchrelbas3  27182  2sqlem6  27367  2sqlem10  27372  dchrisumlem3  27435  dchrisum  27436  dchrmusumlema  27437  dchrvmasumlema  27444  dchrisum0lema  27458  pntibndlem3  27536  pntlem3  27553  pntleml  27555  pnt3  27556  ostth2lem2  27578  ostth  27583  nosupcbv  27647  nosupdm  27649  nosupbnd1lem4  27656  nosupbnd2  27661  noinfcbv  27662  noinfdm  27664  noinfres  27667  noinfbnd1lem1  27668  noinfbnd2  27676  madebdayim  27837  madebday  27849  cofss  27878  coiniss  27879  precsexlem9  28157  onsfi  28287  n0subs  28293  zs12zodd  28394  zs12bday  28396  axcontlem1  28944  axcontlem6  28949  uspgr2wlkeq  29626  crctcshwlkn0  29801  frgrwopreglem5ALT  30301  grpoideu  30488  ubthlem3  30851  adjsym  31812  lnopunilem1  31989  elunop2  31992  lnophm  31998  cnlnadjlem5  32050  mdbr3  32276  mdbr4  32277  dmdbr3  32284  dmdbr4  32285  mddmd2  32288  fprodex01  32800  prodindf  32836  wrdt2ind  32925  toslublem  32944  tosglblem  32946  chnind  32983  chnub  32984  archiabl  33167  isarchiofld  33168  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem2  33215  1arithidom  33501  1arithufdlem3  33510  fedgmul  33620  fldextrspunlsplem  33661  constrconj  33728  qtophaus  33819  lmdvg  33936  esumcvg  34069  unelldsys  34141  ldgenpisyslem1  34146  eulerpartlemsv3  34345  eulerpartlemgvv  34360  signstfvneq0  34556  reprinfz1  34606  tgoldbachgtd  34646  bnj1185  34776  bnj222  34866  bnj517  34868  bnj1452  35035  bnj1463  35038  derangenlem  35151  subfacp1lem6  35165  subfacp1  35166  resconn  35226  cvmscbv  35238  sat1el2xp  35359  untangtr  35694  dfon2lem3  35766  dfon2lem7  35770  nn0prpwlem  36303  neibastop3  36343  fnemeet2  36348  weiunlem2  36444  fvineqsnf1  37391  fvineqsneu  37392  pibt2  37398  phpreu  37591  poimirlem27  37634  heicant  37642  mblfinlem2  37645  ovoliunnfl  37649  voliunnfl  37651  mbfresfi  37653  upixp  37716  sdclem2  37729  fdc  37732  mettrifi  37744  heiborlem5  37802  heiborlem10  37807  heibor  37808  bfp  37811  disjressuc2  38367  cdleme25cv  40345  cdleme40v  40456  aks4d1p7  42064  aks6d1c1p3  42091  aks6d1c1p4  42092  supinf  42223  fsuppind  42571  mzpclval  42706  dford3lem1  43008  fnwe2lem1  43032  aomclem3  43038  aomclem4  43039  aomclem8  43043  dfac11  43044  hbtlem5  43110  nadd1suc  43374  ntrk2imkb  44019  ntrclsk2  44050  ntrclsk4  44054  fnchoice  45016  cncmpmax  45019  wessf1ornlem  45172  disjinfi  45179  rnmptbdd  45232  rnmptbd2  45236  rnmptbd  45243  supxrunb3  45388  unb2ltle  45404  monoord2xrv  45472  uzubioo2  45558  mccl  45589  climsuse  45599  limsupre  45632  limsuppnf  45702  limsupubuz  45704  limsupmnf  45712  limsupre2  45716  limsupmnfuz  45718  limsupre2mpt  45721  limsupre3  45724  limsupre3mpt  45725  limsupre3uzlem  45726  limsupre3uz  45727  limsupreuz  45728  limsupvaluz2  45729  limsupreuzmpt  45730  climuz  45735  lmbr3  45738  limsupge  45752  liminflelimsup  45767  liminfreuz  45794  xlimpnfxnegmnf  45805  cnrefiisp  45821  xlimmnf  45832  xlimpnf  45833  xlimmnfmpt  45834  xlimpnfmpt  45835  dfxlim2  45839  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnprodlem3  45939  stoweidlem7  45998  stoweidlem15  46006  stoweidlem35  46026  wallispilem3  46058  fourierdlem68  46165  fourierdlem71  46168  fourierdlem73  46170  fourierdlem87  46184  fourierdlem100  46197  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem109  46206  fourierdlem112  46209  etransc  46274  qndenserrnbllem  46285  dfsalgen2  46332  subsaliuncl  46349  meaiuninclem  46471  ovnsubaddlem2  46562  hoidmvlelem5  46590  hoidmvle  46591  hoiqssbllem3  46615  vonioo  46673  vonicc  46676  issmf  46719  issmfle  46736  issmfgt  46747  issmfge  46761  smfsuplem2  46803  2reuimp0  47108  uniimafveqt  47375  sbgoldbm  47778  mogoldbb  47779  bgoldbtbndlem4  47802  bgoldbtbnd  47803  nn0sumshdiglem1  48603  ipolub  48969  ipoglb  48972