Theorem cbvralvw 3223

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 2137, ax-11 2154, ax-12 2171, ax-13 2371. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2371. (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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2039	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3063	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2106  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2815  df-ral 3063

This theorem is referenced by:  cbvral2vw  3225  cbvral3vw  3227  reu7  3688  disjxun  5101  reusv3i  5357  wereu2  5628  cnvpo  6237  frpomin  6292  f1mpt  7204  dfwe2  7700  tfinds  7788  frrlem1  8209  wfrlem1OLD  8246  tfrlem1  8314  tfrlem12  8327  rdglem1  8353  tz7.48lem  8379  nneneq  9111  nneneqOLD  9123  marypha1lem  9327  supub  9353  suplub  9354  ordtypecbv  9411  ordtypelem3  9414  ordtypelem9  9420  wemaplem1  9440  brwdom3  9476  ttrclss  9614  ttrclselem2  9620  tcrank  9778  infxpenc2  9916  aceq1  10011  aceq2  10013  dfac5  10022  dfac9  10030  dfac12lem3  10039  kmlem12  10055  kmlem14  10057  cofsmo  10163  infpssrlem4  10200  isfin3ds  10223  isf32lem2  10248  isf32lem11  10257  isf33lem  10260  domtriomlem  10336  axdc3  10348  zorn2lem7  10396  zorn2g  10397  fpwwe2cbv  10524  fpwwecbv  10538  pwfseq  10558  axgroth6  10722  dedekind  11276  suprleub  12079  infregelb  12097  nnsub  12155  uzwo  12790  ublbneg  12812  zsupss  12816  xrub  13185  fsuppmapnn0fiubex  13851  monoord2  13893  faclbnd4lem4  14150  bccl  14176  hashbc  14304  wrdind  14568  wrd2ind  14569  reuccatpfxs1  14593  cau3lem  15199  climmpt2  15415  caucvgrlem  15517  caurcvg2  15522  caucvgb  15524  fsum0diag2  15628  incexclem  15681  cvgrat  15728  mertenslem2  15730  mertens  15731  sqrt2irr  16091  gcdcllem1  16339  lcmfunsnlem1  16473  lcmfunsnlem2lem1  16474  prmind2  16521  prmpwdvds  16736  prmreclem5  16752  prmreclem6  16753  vdwlem7  16819  vdwlem10  16822  vdwlem13  16825  vdwnn  16830  ramcl  16861  isacs2  17493  catpropd  17549  grprinvlem  18488  grprinvd  18489  gsumvalx  18491  mndind  18598  issubg4  18906  isnsg2  18917  elnmz  18924  gsmsymgreqlem2  19172  psgnunilem5  19235  psgnunilem3  19237  efgsdm  19471  gsummptnn0fzfv  19723  pgpfac1lem5  19817  pgpfac1  19818  pgpfac  19822  ablfaclem3  19825  lbsextg  20576  evlslem2  21441  mpfind  21469  cply1mul  21617  mdetuni0  21922  m2cpminvid2lem  22055  mp2pm2mplem4  22110  chcoeffeqlem  22186  cayhamlem3  22188  elcls3  22386  isclo2  22391  neiptopnei  22435  tgcn  22555  subbascn  22557  txcmplem2  22945  kqfvima  23033  kqt0lem  23039  isr0  23040  r0cld  23041  regr1lem2  23043  fbun  23143  flftg  23299  fclsbas  23324  alexsubALTlem2  23351  alexsubALTlem4  23353  ptcmplem4  23358  tsmsxplem1  23456  tsmsxp  23458  ustuqtop  23550  utopsnneip  23552  prdsxmslem2  23837  isclmp  24412  iscau4  24595  caucfil  24599  iscmet3  24609  bcthlem5  24644  bcth  24645  ovolicc2lem5  24837  uniioombllem6  24904  vitali  24929  ismbf3d  24970  itg1climres  25031  itg2seq  25059  itg2monolem1  25067  itg2mono  25070  rolle  25306  dvlipcn  25310  dvivthlem1  25324  ply1divex  25453  fta1g  25484  dgrco  25588  plydivex  25609  fta1  25620  vieta1  25624  ulmcaulem  25705  ulmcau  25706  abelthlem8  25750  wilth  26372  fta  26381  dchrelbas3  26538  2sqlem6  26723  2sqlem10  26728  dchrisumlem3  26791  dchrisum  26792  dchrmusumlema  26793  dchrvmasumlema  26800  dchrisum0lema  26814  pntibndlem3  26892  pntlem3  26909  pntleml  26911  pnt3  26912  ostth2lem2  26934  ostth  26939  nosupcbv  27002  nosupdm  27004  nosupbnd1lem4  27011  nosupbnd2  27016  noinfcbv  27017  noinfdm  27019  noinfres  27022  noinfbnd1lem1  27023  noinfbnd2  27031  madebdayim  27168  madebday  27178  axcontlem1  27742  axcontlem6  27747  uspgr2wlkeq  28423  crctcshwlkn0  28595  frgrwopreglem5ALT  29095  grpoideu  29280  ubthlem3  29643  adjsym  30604  lnopunilem1  30781  elunop2  30784  lnophm  30790  cnlnadjlem5  30842  mdbr3  31068  mdbr4  31069  dmdbr3  31076  dmdbr4  31077  mddmd2  31080  fprodex01  31547  wrdt2ind  31633  toslublem  31658  tosglblem  31660  archiabl  31860  isarchiofld  31938  fedgmul  32146  qtophaus  32229  lmdvg  32346  prodindf  32434  esumcvg  32497  unelldsys  32569  ldgenpisyslem1  32574  eulerpartlemsv3  32773  eulerpartlemgvv  32788  signstfvneq0  32996  reprinfz1  33047  tgoldbachgtd  33087  bnj1185  33217  bnj222  33307  bnj517  33309  bnj1452  33476  bnj1463  33479  derangenlem  33577  subfacp1lem6  33591  subfacp1  33592  resconn  33652  cvmscbv  33664  sat1el2xp  33785  untangtr  34097  dfon2lem3  34176  dfon2lem7  34180  nn0prpwlem  34732  neibastop3  34772  fnemeet2  34777  fvineqsnf1  35819  fvineqsneu  35820  pibt2  35826  phpreu  36000  poimirlem27  36043  heicant  36051  mblfinlem2  36054  ovoliunnfl  36058  voliunnfl  36060  mbfresfi  36062  upixp  36126  sdclem2  36139  fdc  36142  mettrifi  36154  heiborlem5  36212  heiborlem10  36217  heibor  36218  bfp  36221  disjressuc2  36788  cdleme25cv  38759  cdleme40v  38870  aks4d1p7  40478  fsuppind  40674  mzpclval  40957  dford3lem1  41259  fnwe2lem1  41286  aomclem3  41292  aomclem4  41293  aomclem8  41297  dfac11  41298  hbtlem5  41364  ntrk2imkb  42220  ntrclsk2  42251  ntrclsk4  42255  fnchoice  43145  cncmpmax  43148  wessf1ornlem  43308  disjinfi  43317  rnmptbdd  43377  rnmptbd2  43382  rnmptbd  43389  supxrunb3  43539  unb2ltle  43555  monoord2xrv  43624  uzubioo2  43708  mccl  43740  climsuse  43750  limsupre  43783  limsuppnf  43853  limsupubuz  43855  limsupmnf  43863  limsupre2  43867  limsupmnfuz  43869  limsupre2mpt  43872  limsupre3  43875  limsupre3mpt  43876  limsupre3uzlem  43877  limsupre3uz  43878  limsupreuz  43879  limsupvaluz2  43880  limsupreuzmpt  43881  climuz  43886  lmbr3  43889  limsupge  43903  liminflelimsup  43918  liminfreuz  43945  xlimpnfxnegmnf  43956  cnrefiisp  43972  xlimmnf  43983  xlimpnf  43984  xlimmnfmpt  43985  xlimpnfmpt  43986  dfxlim2  43990  dvbdfbdioolem2  44071  dvbdfbdioo  44072  ioodvbdlimc1lem1  44073  ioodvbdlimc1lem2  44074  ioodvbdlimc2lem  44076  dvnprodlem3  44090  stoweidlem7  44149  stoweidlem15  44157  stoweidlem35  44177  wallispilem3  44209  fourierdlem68  44316  fourierdlem71  44319  fourierdlem73  44321  fourierdlem87  44335  fourierdlem100  44348  fourierdlem103  44351  fourierdlem104  44352  fourierdlem107  44355  fourierdlem109  44357  fourierdlem112  44360  etransc  44425  qndenserrnbllem  44436  dfsalgen2  44483  subsaliuncl  44500  meaiuninclem  44622  ovnsubaddlem2  44713  hoidmvlelem5  44741  hoidmvle  44742  hoiqssbllem3  44766  vonioo  44824  vonicc  44827  issmf  44870  issmfle  44887  issmfgt  44898  issmfge  44912  smfsuplem2  44954  2reuimp0  45247  uniimafveqt  45474  sbgoldbm  45877  mogoldbb  45878  bgoldbtbndlem4  45901  bgoldbtbnd  45902  nn0sumshdiglem1  46608  ipolub  46914  ipoglb  46917