Theorem cbvralvw 3216

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3327 with a disjoint variable condition, which does not require ax-10 2147, ax-11 2163, ax-12 2185, 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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2038	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3053	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ral 3053

This theorem is referenced by:  cbvraldva  3218  cbvral2vw  3220  cbvral3vw  3222  cbvral4vw  3223  reu7  3679  cbviinv  4983  disjxun  5084  reusv3i  5342  wereu2  5622  cnvpo  6246  frpomin  6299  f1mpt  7210  dfwe2  7722  tfinds  7805  frrlem1  8230  tfrlem1  8309  tfrlem12  8322  rdglem1  8348  tz7.48lem  8374  cbvixpv  8857  nneneq  9134  marypha1lem  9340  supub  9366  suplub  9367  ordtypecbv  9426  ordtypelem3  9429  ordtypelem9  9435  wemaplem1  9455  brwdom3  9491  ttrclss  9635  ttrclselem2  9641  tcrank  9802  infxpenc2  9938  aceq1  10033  aceq2  10035  dfac5  10045  dfac9  10053  dfac12lem3  10062  kmlem12  10078  kmlem14  10080  cofsmo  10185  infpssrlem4  10222  isfin3ds  10245  isf32lem2  10270  isf32lem11  10279  isf33lem  10282  domtriomlem  10358  axdc3  10370  zorn2lem7  10418  zorn2g  10419  fpwwe2cbv  10547  fpwwecbv  10561  pwfseq  10581  axgroth6  10745  dedekind  11303  suprleub  12116  infregelb  12134  nnsub  12215  uzwo  12855  ublbneg  12877  zsupss  12881  xrub  13258  fsuppmapnn0fiubex  13948  monoord2  13989  faclbnd4lem4  14252  bccl  14278  hashbc  14409  wrdind  14678  wrd2ind  14679  reuccatpfxs1  14703  cau3lem  15311  climmpt2  15529  caucvgrlem  15629  caurcvg2  15634  caucvgb  15636  fsum0diag2  15739  incexclem  15795  cvgrat  15842  mertenslem2  15844  mertens  15845  sqrt2irr  16210  gcdcllem1  16462  lcmfunsnlem1  16600  lcmfunsnlem2lem1  16601  prmind2  16648  prmpwdvds  16869  prmreclem5  16885  prmreclem6  16886  vdwlem7  16952  vdwlem10  16955  vdwlem13  16958  vdwnn  16963  ramcl  16994  isacs2  17613  catpropd  17669  chnind  18581  chnub  18582  grpinvalem  18635  grpinva  18636  gsumvalx  18638  mndind  18790  issubg4  19115  isnsg2  19125  elnmz  19132  gsmsymgreqlem2  19400  psgnunilem5  19463  psgnunilem3  19465  efgsdm  19699  gsummptnn0fzfv  19956  pgpfac1lem5  20050  pgpfac1  20051  pgpfac  20055  ablfaclem3  20058  lbsextg  21155  evlslem2  22070  mpfind  22106  cply1mul  22274  mdetuni0  22599  m2cpminvid2lem  22732  mp2pm2mplem4  22787  chcoeffeqlem  22863  cayhamlem3  22865  elcls3  23061  isclo2  23066  neiptopnei  23110  tgcn  23230  subbascn  23232  txcmplem2  23620  kqfvima  23708  kqt0lem  23714  isr0  23715  r0cld  23716  regr1lem2  23718  fbun  23818  flftg  23974  fclsbas  23999  alexsubALTlem2  24026  alexsubALTlem4  24028  ptcmplem4  24033  tsmsxplem1  24131  tsmsxp  24133  ustuqtop  24224  utopsnneip  24226  prdsxmslem2  24507  isclmp  25077  iscau4  25259  caucfil  25263  iscmet3  25273  bcthlem5  25308  bcth  25309  ovolicc2lem5  25501  uniioombllem6  25568  vitali  25593  ismbf3d  25634  itg1climres  25694  itg2seq  25722  itg2monolem1  25730  itg2mono  25733  rolle  25970  dvlipcn  25974  dvivthlem1  25988  ply1divex  26115  fta1g  26148  dgrco  26253  plydivex  26277  fta1  26288  vieta1  26292  ulmcaulem  26375  ulmcau  26376  abelthlem8  26420  wilth  27051  fta  27060  fsumdvdsmul  27175  dchrelbas3  27218  2sqlem6  27403  2sqlem10  27408  dchrisumlem3  27471  dchrisum  27472  dchrmusumlema  27473  dchrvmasumlema  27480  dchrisum0lema  27494  pntibndlem3  27572  pntlem3  27589  pntleml  27591  pnt3  27592  ostth2lem2  27614  ostth  27619  nosupcbv  27683  nosupdm  27685  nosupbnd1lem4  27692  nosupbnd2  27697  noinfcbv  27698  noinfdm  27700  noinfres  27703  noinfbnd1lem1  27704  noinfbnd2  27712  madebdayim  27897  madebday  27909  cofss  27939  coiniss  27940  cutminmax  27945  precsexlem9  28224  onsfi  28365  n0subs  28372  bdayfinbndcbv  28475  bdayfinbndlem2  28477  z12zsodd  28491  axcontlem1  29050  axcontlem6  29055  uspgr2wlkeq  29732  crctcshwlkn0  29907  frgrwopreglem5ALT  30410  grpoideu  30598  ubthlem3  30961  adjsym  31922  lnopunilem1  32099  elunop2  32102  lnophm  32108  cnlnadjlem5  32160  mdbr3  32386  mdbr4  32387  dmdbr3  32394  dmdbr4  32395  mddmd2  32398  fprodex01  32916  prodindf  32940  wrdt2ind  33031  toslublem  33050  tosglblem  33052  archiabl  33277  isarchiofld  33278  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem4  33324  elrgspnsubrunlem2  33327  1arithidom  33615  1arithufdlem3  33624  vietadeg1  33740  vieta  33742  fedgmul  33794  fldextrspunlsplem  33836  constrconj  33908  qtophaus  33999  lmdvg  34116  esumcvg  34249  unelldsys  34321  ldgenpisyslem1  34326  eulerpartlemsv3  34524  eulerpartlemgvv  34539  signstfvneq0  34735  reprinfz1  34785  tgoldbachgtd  34825  bnj1185  34954  bnj222  35044  bnj517  35046  bnj1452  35213  bnj1463  35216  derangenlem  35372  subfacp1lem6  35386  subfacp1  35387  resconn  35447  cvmscbv  35459  sat1el2xp  35580  untangtr  35915  dfon2lem3  35984  dfon2lem7  35988  nn0prpwlem  36523  neibastop3  36563  fnemeet2  36568  weiunlem  36664  mh-infprim2bi  36748  mh-infprim3bi  36749  fvineqsnf1  37743  fvineqsneu  37744  pibt2  37750  phpreu  37942  poimirlem27  37985  heicant  37993  mblfinlem2  37996  ovoliunnfl  38000  voliunnfl  38002  mbfresfi  38004  upixp  38067  sdclem2  38080  fdc  38083  mettrifi  38095  heiborlem5  38153  heiborlem10  38158  heibor  38159  bfp  38162  disjressuc2  38749  cdleme25cv  40821  cdleme40v  40932  aks4d1p7  42539  aks6d1c1p3  42566  aks6d1c1p4  42567  supinf  42698  fsuppind  43040  mzpclval  43174  dford3lem1  43475  fnwe2lem1  43499  aomclem3  43505  aomclem4  43506  aomclem8  43510  dfac11  43511  hbtlem5  43577  nadd1suc  43841  ntrk2imkb  44485  ntrclsk2  44516  ntrclsk4  44520  fnchoice  45481  cncmpmax  45484  wessf1ornlem  45636  disjinfi  45643  rnmptbdd  45695  rnmptbd2  45699  rnmptbd  45706  supxrunb3  45849  unb2ltle  45864  monoord2xrv  45932  uzubioo2  46018  mccl  46049  climsuse  46059  limsupre  46090  limsuppnf  46160  limsupubuz  46162  limsupmnf  46170  limsupre2  46174  limsupmnfuz  46176  limsupre2mpt  46179  limsupre3  46182  limsupre3mpt  46183  limsupre3uzlem  46184  limsupre3uz  46185  limsupreuz  46186  limsupvaluz2  46187  limsupreuzmpt  46188  climuz  46193  lmbr3  46196  limsupge  46210  liminflelimsup  46225  liminfreuz  46252  xlimpnfxnegmnf  46263  cnrefiisp  46279  xlimmnf  46290  xlimpnf  46291  xlimmnfmpt  46292  xlimpnfmpt  46293  dfxlim2  46297  dvbdfbdioolem2  46378  dvbdfbdioo  46379  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnprodlem3  46397  stoweidlem7  46456  stoweidlem15  46464  stoweidlem35  46484  wallispilem3  46516  fourierdlem68  46623  fourierdlem71  46626  fourierdlem73  46628  fourierdlem87  46642  fourierdlem100  46655  fourierdlem103  46658  fourierdlem104  46659  fourierdlem107  46662  fourierdlem109  46664  fourierdlem112  46667  etransc  46732  qndenserrnbllem  46743  dfsalgen2  46790  subsaliuncl  46807  meaiuninclem  46929  ovnsubaddlem2  47020  hoidmvlelem5  47048  hoidmvle  47049  hoiqssbllem3  47073  vonioo  47131  vonicc  47134  issmf  47177  issmfle  47194  issmfgt  47205  issmfge  47219  smfsuplem2  47261  chnerlem1  47331  2reuimp0  47577  uniimafveqt  47856  sbgoldbm  48275  mogoldbb  48276  bgoldbtbndlem4  48299  bgoldbtbnd  48300  nn0sumshdiglem1  49112  ipolub  49478  ipoglb  49481