Theorem cbvralvw 3242

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3351 with a disjoint variable condition, which does not require ax-10 2178, ax-11 2194, ax-12 2215, ax-13 2403. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2403. (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 2845	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2069	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3079	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837  df-ral 3079

This theorem is used by:  cbvraldva  3244  cbvral2vw  3246  cbvral3vw  3248  cbvral4vw  3249  reu7  3693  cbviinv  5002  disjxun  5105  reusv3i  5373  wereu2  5656  cnvpo  6289  frpomin  6342  f1mpt  7261  dfwe2  7776  tfinds  7859  frrlem1  8288  tfrlem1  8367  tfrlem12  8381  rdglem1  8407  tz7.48lem  8433  cbvixpv  8925  nneneq  9203  marypha1lem  9406  supub  9432  suplub  9433  ordtypecbv  9492  ordtypelem3  9495  ordtypelem9  9501  wemaplem1  9521  brwdom3  9557  ttrclss  9702  ttrclselem2  9708  tcrank  9869  infxpenc2  10028  aceq1  10123  aceq2  10125  dfac5  10134  dfac9  10142  dfac12lem3  10151  kmlem12  10167  kmlem14  10169  cofsmo  10274  infpssrlem4  10311  isfin3ds  10334  isf32lem2  10359  isf32lem11  10368  isf33lem  10371  domtriomlem  10447  axdc3  10459  zorn2lem7  10507  zorn2g  10508  fpwwe2cbv  10642  fpwwecbv  10656  pwfseq  10676  axgroth6  10840  dedekind  11400  suprleub  12208  infregelb  12226  nnsub  12307  uzwo  12963  ublbneg  12985  zsupss  12989  xrub  13366  fsuppmapnn0fiubex  14058  monoord2  14099  faclbnd4lem4  14362  bccl  14388  hashbc  14520  wrdind  14793  wrd2ind  14794  reuccatpfxs1  14818  cau3lem  15444  climmpt2  15662  caucvgrlem  15762  caurcvg2  15767  caucvgb  15769  fsum0diag2  15871  incexclem  15927  cvgrat  15974  mertenslem2  15976  mertens  15977  sqrt2irr  16341  gcdcllem1  16593  lcmfunsnlem1  16731  lcmfunsnlem2lem1  16732  prmind2  16779  prmpwdvds  17000  prmreclem5  17016  prmreclem6  17017  vdwlem7  17083  vdwlem10  17086  vdwlem13  17089  vdwnn  17094  ramcl  17125  isacs2  17745  catpropd  17801  chnind  18713  chnub  18714  grpinvalem  18771  grpinva  18772  gsumvalx  18780  mndind  18938  issubg4  19270  isnsg2  19280  elnmz  19287  gsmsymgreqlem2  19559  psgnunilem5  19622  psgnunilem3  19624  efgsdm  19858  gsummptnn0fzfv  20115  pgpfac1lem5  20209  pgpfac1  20210  pgpfac  20214  ablfaclem3  20217  lbsextg  21350  evlslem2  22296  mpfind  22332  cply1mul  22522  mdetuni0  22844  m2cpminvid2lem  22980  mp2pm2mplem4  23035  chcoeffeqlem  23111  cayhamlem3  23113  elcls3  23309  isclo2  23314  neiptopnei  23358  tgcn  23478  subbascn  23480  txcmplem2  23869  kqfvima  23957  kqt0lem  23963  isr0  23964  r0cld  23965  regr1lem2  23967  fbun  24067  flftg  24223  fclsbas  24248  alexsubALTlem2  24275  alexsubALTlem4  24277  ptcmplem4  24282  tsmsxplem1  24380  tsmsxp  24382  ustuqtop  24473  utopsnneip  24475  prdsxmslem2  24756  isclmp  25326  iscau4  25508  caucfil  25512  iscmet3  25522  bcthlem5  25557  bcth  25558  ovolicc2lem5  25750  uniioombllem6  25817  vitali  25842  ismbf3d  25883  itg1climres  25943  itg2seq  25971  itg2monolem1  25979  itg2mono  25982  rolle  26219  dvlipcn  26223  dvivthlem1  26237  ply1divex  26364  fta1g  26397  dgrco  26502  plydivex  26528  fta1  26539  vieta1  26543  ulmcaulem  26627  ulmcau  26628  abelthlem8  26672  wilth  27305  fta  27314  fsumdvdsmul  27429  dchrelbas3  27472  2sqlem6  27657  2sqlem10  27662  dchrisumlem3  27725  dchrisum  27726  dchrmusumlema  27727  dchrvmasumlema  27734  dchrisum0lema  27748  pntibndlem3  27826  pntlem3  27843  pntleml  27845  pnt3  27846  ostth2lem2  27868  ostth  27873  nosupcbv  27936  nosupdm  27938  nosupbnd1lem4  27945  nosupbnd2  27950  noinfcbv  27951  noinfdm  27953  noinfres  27956  noinfbnd1lem1  27957  noinfbnd2  27965  madebdayim  28151  madebday  28163  cofss  28193  coiniss  28194  cutminmax  28199  precsexlem9  28478  onsfi  28619  n0subs  28626  bdayfinbndcbv  28729  bdayfinbndlem2  28731  z12zsodd  28745  axcontlem1  29407  axcontlem6  29412  uspgr2wlkeq  30091  crctcshwlkn0  30275  frgrwopreglem5ALT  30788  grpoideu  30976  ubthlem3  31339  adjsym  32300  lnopunilem1  32477  elunop2  32480  lnophm  32486  cnlnadjlem5  32538  mdbr3  32764  mdbr4  32765  dmdbr3  32772  dmdbr4  32773  mddmd2  32776  fprodex01  33282  prodindf  33295  wrdt2ind  33382  toslublem  33399  tosglblem  33401  archiabl  33625  isarchiofld  33626  elrgspnlem1  33669  elrgspnlem2  33670  elrgspnlem4  33672  elrgspnsubrunlem2  33675  1arithidom  33934  1arithufdlem3  33943  vietadeg1  34075  vieta  34077  fedgmul  34128  fldextrspunlsplem  34170  constrconj  34242  qtophaus  34333  lmdvg  34450  esumcvg  34583  unelldsys  34656  ldgenpisyslem1  34661  eulerpartlemsv3  34859  eulerpartlemgvv  34874  signstfvneq0  35067  reprinfz1  35117  tgoldbachgtd  35157  bnj1185  35289  bnj222  35379  bnj517  35381  bnj1452  35548  bnj1463  35551  derangenlem  35737  subfacp1lem6  35751  subfacp1  35752  resconn  35812  cvmscbv  35824  sat1el2xp  35945  untangtr  36280  dfon2lem3  36349  dfon2lem7  36353  nadddilem2  36788  nadddilem4  36790  nn0prpwlem  36928  neibastop3  36968  fnemeet2  36973  weiunlem  37069  mh-infprim2bi  37153  mh-infprim3bi  37154  fvineqsnf1  38151  fvineqsneu  38152  pibt2  38158  phpreu  38345  poimirlem27  38383  heicant  38391  mblfinlem2  38394  ovoliunnfl  38398  voliunnfl  38400  mbfresfi  38402  upixp  38466  sdclem2  38479  fdc  38482  mettrifi  38494  heiborlem5  38552  heiborlem10  38557  heibor  38558  bfp  38561  disjressuc2  39146  cdleme25cv  41218  cdleme40v  41329  aks4d1p7  42936  aks6d1c1p3  42963  aks6d1c1p4  42964  supinf  43096  fsuppind  43423  mzpclval  43557  dford3lem1  43854  fnwe2lem1  43878  aomclem3  43884  aomclem4  43885  aomclem8  43889  dfac11  43890  hbtlem5  43956  nadd1suc  44220  ntrk2imkb  44864  ntrclsk2  44895  ntrclsk4  44899  fnchoice  45850  cncmpmax  45853  wessf1ornlem  46004  disjinfi  46011  rnmptbdd  46061  rnmptbd2  46065  rnmptbd  46072  supxrunb3  46215  unb2ltle  46230  monoord2xrv  46298  uzubioo2  46384  mccl  46415  climsuse  46425  limsupre  46456  limsuppnf  46526  limsupubuz  46528  limsupmnf  46536  limsupre2  46540  limsupmnfuz  46542  limsupre2mpt  46545  limsupre3  46548  limsupre3mpt  46549  limsupre3uzlem  46550  limsupre3uz  46551  limsupreuz  46552  limsupvaluz2  46553  limsupreuzmpt  46554  climuz  46559  lmbr3  46562  limsupge  46576  liminflelimsup  46591  liminfreuz  46618  xlimpnfxnegmnf  46629  cnrefiisp  46645  xlimmnf  46656  xlimpnf  46657  xlimmnfmpt  46658  xlimpnfmpt  46659  dfxlim2  46663  dvbdfbdioolem2  46744  dvbdfbdioo  46745  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  dvnprodlem3  46763  stoweidlem7  46822  stoweidlem15  46830  stoweidlem35  46850  wallispilem3  46882  fourierdlem68  46989  fourierdlem71  46992  fourierdlem73  46994  fourierdlem87  47008  fourierdlem100  47021  fourierdlem103  47024  fourierdlem104  47025  fourierdlem107  47028  fourierdlem109  47030  fourierdlem112  47033  etransc  47098  qndenserrnbllem  47109  dfsalgen2  47156  subsaliuncl  47173  meaiuninclem  47295  ovnsubaddlem2  47386  hoidmvlelem5  47414  hoidmvle  47415  hoiqssbllem3  47439  vonioo  47497  vonicc  47500  issmf  47543  issmfle  47560  issmfgt  47571  issmfge  47585  smfsuplem2  47627  chnerlem1  47697  tmachlem-agreesn  47762  2reuimp0  47989  uniimafveqt  48268  sbgoldbm  48687  mogoldbb  48688  bgoldbtbndlem4  48711  bgoldbtbnd  48712  nn0sumshdiglem1  49538  ipolub  49901  ipoglb  49904