Theorem cbvralvw 3232

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3358 with a disjoint variable condition, which does not require ax-10 2129, ax-11 2146, ax-12 2166, ax-13 2366. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2366. (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 2812	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 343	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2031	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3059	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3059	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531   ∈ wcel 2098  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2806  df-ral 3059

This theorem is referenced by:  cbvraldva  3234  cbvral2vw  3236  cbvral3vw  3238  cbvral4vw  3239  reu7  3729  disjxun  5150  reusv3i  5408  wereu2  5679  cnvpo  6296  frpomin  6351  f1mpt  7277  dfwe2  7784  tfinds  7872  frrlem1  8300  wfrlem1OLD  8337  tfrlem1  8405  tfrlem12  8418  rdglem1  8444  tz7.48lem  8470  nneneq  9242  nneneqOLD  9254  marypha1lem  9466  supub  9492  suplub  9493  ordtypecbv  9550  ordtypelem3  9553  ordtypelem9  9559  wemaplem1  9579  brwdom3  9615  ttrclss  9753  ttrclselem2  9759  tcrank  9917  infxpenc2  10055  aceq1  10150  aceq2  10152  dfac5  10161  dfac9  10169  dfac12lem3  10178  kmlem12  10194  kmlem14  10196  cofsmo  10302  infpssrlem4  10339  isfin3ds  10362  isf32lem2  10387  isf32lem11  10396  isf33lem  10399  domtriomlem  10475  axdc3  10487  zorn2lem7  10535  zorn2g  10536  fpwwe2cbv  10663  fpwwecbv  10677  pwfseq  10697  axgroth6  10861  dedekind  11417  suprleub  12220  infregelb  12238  nnsub  12296  uzwo  12935  ublbneg  12957  zsupss  12961  xrub  13333  fsuppmapnn0fiubex  13999  monoord2  14040  faclbnd4lem4  14297  bccl  14323  hashbc  14454  wrdind  14714  wrd2ind  14715  reuccatpfxs1  14739  cau3lem  15343  climmpt2  15559  caucvgrlem  15661  caurcvg2  15666  caucvgb  15668  fsum0diag2  15771  incexclem  15824  cvgrat  15871  mertenslem2  15873  mertens  15874  sqrt2irr  16235  gcdcllem1  16483  lcmfunsnlem1  16617  lcmfunsnlem2lem1  16618  prmind2  16665  prmpwdvds  16882  prmreclem5  16898  prmreclem6  16899  vdwlem7  16965  vdwlem10  16968  vdwlem13  16971  vdwnn  16976  ramcl  17007  isacs2  17642  catpropd  17698  grpinvalem  18642  grpinva  18643  gsumvalx  18645  mndind  18794  issubg4  19114  isnsg2  19125  elnmz  19132  gsmsymgreqlem2  19400  psgnunilem5  19463  psgnunilem3  19465  efgsdm  19699  gsummptnn0fzfv  19956  pgpfac1lem5  20050  pgpfac1  20051  pgpfac  20055  ablfaclem3  20058  lbsextg  21064  evlslem2  22042  mpfind  22070  cply1mul  22234  mdetuni0  22551  m2cpminvid2lem  22684  mp2pm2mplem4  22739  chcoeffeqlem  22815  cayhamlem3  22817  elcls3  23015  isclo2  23020  neiptopnei  23064  tgcn  23184  subbascn  23186  txcmplem2  23574  kqfvima  23662  kqt0lem  23668  isr0  23669  r0cld  23670  regr1lem2  23672  fbun  23772  flftg  23928  fclsbas  23953  alexsubALTlem2  23980  alexsubALTlem4  23982  ptcmplem4  23987  tsmsxplem1  24085  tsmsxp  24087  ustuqtop  24179  utopsnneip  24181  prdsxmslem2  24466  isclmp  25052  iscau4  25235  caucfil  25239  iscmet3  25249  bcthlem5  25284  bcth  25285  ovolicc2lem5  25478  uniioombllem6  25545  vitali  25570  ismbf3d  25611  itg1climres  25672  itg2seq  25700  itg2monolem1  25708  itg2mono  25711  rolle  25950  dvlipcn  25955  dvivthlem1  25969  ply1divex  26100  fta1g  26132  dgrco  26238  plydivex  26260  fta1  26271  vieta1  26275  ulmcaulem  26358  ulmcau  26359  abelthlem8  26404  wilth  27031  fta  27040  fsumdvdsmul  27155  dchrelbas3  27199  2sqlem6  27384  2sqlem10  27389  dchrisumlem3  27452  dchrisum  27453  dchrmusumlema  27454  dchrvmasumlema  27461  dchrisum0lema  27475  pntibndlem3  27553  pntlem3  27570  pntleml  27572  pnt3  27573  ostth2lem2  27595  ostth  27600  nosupcbv  27663  nosupdm  27665  nosupbnd1lem4  27672  nosupbnd2  27677  noinfcbv  27678  noinfdm  27680  noinfres  27683  noinfbnd1lem1  27684  noinfbnd2  27692  madebdayim  27842  madebday  27854  cofss  27878  coiniss  27879  precsexlem9  28141  axcontlem1  28803  axcontlem6  28808  uspgr2wlkeq  29488  crctcshwlkn0  29660  frgrwopreglem5ALT  30160  grpoideu  30347  ubthlem3  30710  adjsym  31671  lnopunilem1  31848  elunop2  31851  lnophm  31857  cnlnadjlem5  31909  mdbr3  32135  mdbr4  32136  dmdbr3  32143  dmdbr4  32144  mddmd2  32147  fprodex01  32617  wrdt2ind  32703  toslublem  32728  tosglblem  32730  archiabl  32935  isarchiofld  33064  fedgmul  33370  qtophaus  33478  lmdvg  33595  prodindf  33683  esumcvg  33746  unelldsys  33818  ldgenpisyslem1  33823  eulerpartlemsv3  34022  eulerpartlemgvv  34037  signstfvneq0  34245  reprinfz1  34295  tgoldbachgtd  34335  bnj1185  34465  bnj222  34555  bnj517  34557  bnj1452  34724  bnj1463  34727  derangenlem  34822  subfacp1lem6  34836  subfacp1  34837  resconn  34897  cvmscbv  34909  sat1el2xp  35030  untangtr  35349  dfon2lem3  35422  dfon2lem7  35426  nn0prpwlem  35847  neibastop3  35887  fnemeet2  35892  fvineqsnf1  36930  fvineqsneu  36931  pibt2  36937  phpreu  37118  poimirlem27  37161  heicant  37169  mblfinlem2  37172  ovoliunnfl  37176  voliunnfl  37178  mbfresfi  37180  upixp  37243  sdclem2  37256  fdc  37259  mettrifi  37271  heiborlem5  37329  heiborlem10  37334  heibor  37335  bfp  37338  disjressuc2  37900  cdleme25cv  39871  cdleme40v  39982  aks4d1p7  41594  aks6d1c1p3  41621  aks6d1c1p4  41622  fsuppind  41872  mzpclval  42194  dford3lem1  42496  fnwe2lem1  42523  aomclem3  42529  aomclem4  42530  aomclem8  42534  dfac11  42535  hbtlem5  42601  nadd1suc  42870  ntrk2imkb  43516  ntrclsk2  43547  ntrclsk4  43551  fnchoice  44440  cncmpmax  44443  wessf1ornlem  44606  disjinfi  44613  rnmptbdd  44668  rnmptbd2  44672  rnmptbd  44679  supxrunb3  44828  unb2ltle  44844  monoord2xrv  44913  uzubioo2  45001  mccl  45033  climsuse  45043  limsupre  45076  limsuppnf  45146  limsupubuz  45148  limsupmnf  45156  limsupre2  45160  limsupmnfuz  45162  limsupre2mpt  45165  limsupre3  45168  limsupre3mpt  45169  limsupre3uzlem  45170  limsupre3uz  45171  limsupreuz  45172  limsupvaluz2  45173  limsupreuzmpt  45174  climuz  45179  lmbr3  45182  limsupge  45196  liminflelimsup  45211  liminfreuz  45238  xlimpnfxnegmnf  45249  cnrefiisp  45265  xlimmnf  45276  xlimpnf  45277  xlimmnfmpt  45278  xlimpnfmpt  45279  dfxlim2  45283  dvbdfbdioolem2  45364  dvbdfbdioo  45365  ioodvbdlimc1lem1  45366  ioodvbdlimc1lem2  45367  ioodvbdlimc2lem  45369  dvnprodlem3  45383  stoweidlem7  45442  stoweidlem15  45450  stoweidlem35  45470  wallispilem3  45502  fourierdlem68  45609  fourierdlem71  45612  fourierdlem73  45614  fourierdlem87  45628  fourierdlem100  45641  fourierdlem103  45644  fourierdlem104  45645  fourierdlem107  45648  fourierdlem109  45650  fourierdlem112  45653  etransc  45718  qndenserrnbllem  45729  dfsalgen2  45776  subsaliuncl  45793  meaiuninclem  45915  ovnsubaddlem2  46006  hoidmvlelem5  46034  hoidmvle  46035  hoiqssbllem3  46059  vonioo  46117  vonicc  46120  issmf  46163  issmfle  46180  issmfgt  46191  issmfge  46205  smfsuplem2  46247  2reuimp0  46541  uniimafveqt  46768  sbgoldbm  47171  mogoldbb  47172  bgoldbtbndlem4  47195  bgoldbtbnd  47196  nn0sumshdiglem1  47790  ipolub  48095  ipoglb  48098