Theorem cbvralvw 3225

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   ∈ wcel 2099  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-clel 2803  df-ral 3052

This theorem is referenced by:  cbvraldva  3227  cbvral2vw  3229  cbvral3vw  3231  cbvral4vw  3232  reu7  3726  disjxun  5151  reusv3i  5408  wereu2  5679  cnvpo  6298  frpomin  6353  f1mpt  7276  dfwe2  7782  tfinds  7870  frrlem1  8301  wfrlem1OLD  8338  tfrlem1  8406  tfrlem12  8419  rdglem1  8445  tz7.48lem  8471  nneneq  9243  nneneqOLD  9255  marypha1lem  9476  supub  9502  suplub  9503  ordtypecbv  9560  ordtypelem3  9563  ordtypelem9  9569  wemaplem1  9589  brwdom3  9625  ttrclss  9763  ttrclselem2  9769  tcrank  9927  infxpenc2  10065  aceq1  10160  aceq2  10162  dfac5  10171  dfac9  10179  dfac12lem3  10188  kmlem12  10204  kmlem14  10206  cofsmo  10312  infpssrlem4  10349  isfin3ds  10372  isf32lem2  10397  isf32lem11  10406  isf33lem  10409  domtriomlem  10485  axdc3  10497  zorn2lem7  10545  zorn2g  10546  fpwwe2cbv  10673  fpwwecbv  10687  pwfseq  10707  axgroth6  10871  dedekind  11427  suprleub  12232  infregelb  12250  nnsub  12308  uzwo  12947  ublbneg  12969  zsupss  12973  xrub  13345  fsuppmapnn0fiubex  14012  monoord2  14053  faclbnd4lem4  14313  bccl  14339  hashbc  14470  wrdind  14730  wrd2ind  14731  reuccatpfxs1  14755  cau3lem  15359  climmpt2  15575  caucvgrlem  15677  caurcvg2  15682  caucvgb  15684  fsum0diag2  15787  incexclem  15840  cvgrat  15887  mertenslem2  15889  mertens  15890  sqrt2irr  16251  gcdcllem1  16499  lcmfunsnlem1  16638  lcmfunsnlem2lem1  16639  prmind2  16686  prmpwdvds  16906  prmreclem5  16922  prmreclem6  16923  vdwlem7  16989  vdwlem10  16992  vdwlem13  16995  vdwnn  17000  ramcl  17031  isacs2  17666  catpropd  17722  grpinvalem  18666  grpinva  18667  gsumvalx  18669  mndind  18818  issubg4  19139  isnsg2  19150  elnmz  19157  gsmsymgreqlem2  19429  psgnunilem5  19492  psgnunilem3  19494  efgsdm  19728  gsummptnn0fzfv  19985  pgpfac1lem5  20079  pgpfac1  20080  pgpfac  20084  ablfaclem3  20087  lbsextg  21143  evlslem2  22094  mpfind  22122  cply1mul  22287  mdetuni0  22614  m2cpminvid2lem  22747  mp2pm2mplem4  22802  chcoeffeqlem  22878  cayhamlem3  22880  elcls3  23078  isclo2  23083  neiptopnei  23127  tgcn  23247  subbascn  23249  txcmplem2  23637  kqfvima  23725  kqt0lem  23731  isr0  23732  r0cld  23733  regr1lem2  23735  fbun  23835  flftg  23991  fclsbas  24016  alexsubALTlem2  24043  alexsubALTlem4  24045  ptcmplem4  24050  tsmsxplem1  24148  tsmsxp  24150  ustuqtop  24242  utopsnneip  24244  prdsxmslem2  24529  isclmp  25115  iscau4  25298  caucfil  25302  iscmet3  25312  bcthlem5  25347  bcth  25348  ovolicc2lem5  25541  uniioombllem6  25608  vitali  25633  ismbf3d  25674  itg1climres  25735  itg2seq  25763  itg2monolem1  25771  itg2mono  25774  rolle  26013  dvlipcn  26018  dvivthlem1  26032  ply1divex  26164  fta1g  26197  dgrco  26303  plydivex  26325  fta1  26336  vieta1  26340  ulmcaulem  26423  ulmcau  26424  abelthlem8  26469  wilth  27099  fta  27108  fsumdvdsmul  27223  dchrelbas3  27267  2sqlem6  27452  2sqlem10  27457  dchrisumlem3  27520  dchrisum  27521  dchrmusumlema  27522  dchrvmasumlema  27529  dchrisum0lema  27543  pntibndlem3  27621  pntlem3  27638  pntleml  27640  pnt3  27641  ostth2lem2  27663  ostth  27668  nosupcbv  27732  nosupdm  27734  nosupbnd1lem4  27741  nosupbnd2  27746  noinfcbv  27747  noinfdm  27749  noinfres  27752  noinfbnd1lem1  27753  noinfbnd2  27761  madebdayim  27911  madebday  27923  cofss  27947  coiniss  27948  precsexlem9  28214  n0subs  28326  axcontlem1  28898  axcontlem6  28903  uspgr2wlkeq  29583  crctcshwlkn0  29755  frgrwopreglem5ALT  30255  grpoideu  30442  ubthlem3  30805  adjsym  31766  lnopunilem1  31943  elunop2  31946  lnophm  31952  cnlnadjlem5  32004  mdbr3  32230  mdbr4  32231  dmdbr3  32238  dmdbr4  32239  mddmd2  32242  fprodex01  32726  wrdt2ind  32817  toslublem  32842  tosglblem  32844  chnind  32880  chnub  32881  archiabl  33063  isarchiofld  33195  1arithidom  33412  1arithufdlem3  33421  fedgmul  33526  constrconj  33603  qtophaus  33651  lmdvg  33768  prodindf  33856  esumcvg  33919  unelldsys  33991  ldgenpisyslem1  33996  eulerpartlemsv3  34195  eulerpartlemgvv  34210  signstfvneq0  34418  reprinfz1  34468  tgoldbachgtd  34508  bnj1185  34638  bnj222  34728  bnj517  34730  bnj1452  34897  bnj1463  34900  derangenlem  34999  subfacp1lem6  35013  subfacp1  35014  resconn  35074  cvmscbv  35086  sat1el2xp  35207  untangtr  35536  dfon2lem3  35609  dfon2lem7  35613  nn0prpwlem  36034  neibastop3  36074  fnemeet2  36079  fvineqsnf1  37117  fvineqsneu  37118  pibt2  37124  phpreu  37305  poimirlem27  37348  heicant  37356  mblfinlem2  37359  ovoliunnfl  37363  voliunnfl  37365  mbfresfi  37367  upixp  37430  sdclem2  37443  fdc  37446  mettrifi  37458  heiborlem5  37516  heiborlem10  37521  heibor  37522  bfp  37525  disjressuc2  38086  cdleme25cv  40057  cdleme40v  40168  aks4d1p7  41782  aks6d1c1p3  41808  aks6d1c1p4  41809  supinf  41966  fsuppind  42062  mzpclval  42382  dford3lem1  42684  fnwe2lem1  42711  aomclem3  42717  aomclem4  42718  aomclem8  42722  dfac11  42723  hbtlem5  42789  nadd1suc  43058  ntrk2imkb  43704  ntrclsk2  43735  ntrclsk4  43739  fnchoice  44628  cncmpmax  44631  wessf1ornlem  44792  disjinfi  44799  rnmptbdd  44854  rnmptbd2  44858  rnmptbd  44865  supxrunb3  45014  unb2ltle  45030  monoord2xrv  45099  uzubioo2  45187  mccl  45219  climsuse  45229  limsupre  45262  limsuppnf  45332  limsupubuz  45334  limsupmnf  45342  limsupre2  45346  limsupmnfuz  45348  limsupre2mpt  45351  limsupre3  45354  limsupre3mpt  45355  limsupre3uzlem  45356  limsupre3uz  45357  limsupreuz  45358  limsupvaluz2  45359  limsupreuzmpt  45360  climuz  45365  lmbr3  45368  limsupge  45382  liminflelimsup  45397  liminfreuz  45424  xlimpnfxnegmnf  45435  cnrefiisp  45451  xlimmnf  45462  xlimpnf  45463  xlimmnfmpt  45464  xlimpnfmpt  45465  dfxlim2  45469  dvbdfbdioolem2  45550  dvbdfbdioo  45551  ioodvbdlimc1lem1  45552  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  dvnprodlem3  45569  stoweidlem7  45628  stoweidlem15  45636  stoweidlem35  45656  wallispilem3  45688  fourierdlem68  45795  fourierdlem71  45798  fourierdlem73  45800  fourierdlem87  45814  fourierdlem100  45827  fourierdlem103  45830  fourierdlem104  45831  fourierdlem107  45834  fourierdlem109  45836  fourierdlem112  45839  etransc  45904  qndenserrnbllem  45915  dfsalgen2  45962  subsaliuncl  45979  meaiuninclem  46101  ovnsubaddlem2  46192  hoidmvlelem5  46220  hoidmvle  46221  hoiqssbllem3  46245  vonioo  46303  vonicc  46306  issmf  46349  issmfle  46366  issmfgt  46377  issmfge  46391  smfsuplem2  46433  2reuimp0  46727  uniimafveqt  46953  sbgoldbm  47356  mogoldbb  47357  bgoldbtbndlem4  47380  bgoldbtbnd  47381  nn0sumshdiglem1  48009  ipolub  48314  ipoglb  48317