Theorem cbvralvw 3241

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

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

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 2836  df-ral 3078

This theorem is used by:  cbvraldva  3243  cbvral2vw  3245  cbvral3vw  3247  cbvral4vw  3248  reu7  3690  cbviinv  4998  disjxun  5101  reusv3i  5366  wereu2  5648  cnvpo  6290  frpomin  6343  f1mpt  7265  dfwe2  7788  tfinds  7871  fnwe2lem2  8146  frrlem1  8304  tfrlem1  8383  tfrlem12  8397  rdglem1  8423  tz7.48lemOLD  8451  cbvixpv  8943  nneneq  9221  marypha1lem  9425  supub  9451  suplub  9452  ordtypecbv  9511  ordtypelem3  9514  ordtypelem9  9520  wemaplem1  9540  brwdom3  9576  ttrclss  9721  ttrclselem2  9727  tcrank  9901  infxpenc2  10101  aceq1  10196  aceq2  10198  dfac5  10207  dfac9  10215  dfac12lem3  10224  kmlem12  10240  kmlem14  10242  cofsmo  10347  infpssrlem4  10384  isfin3ds  10407  isf32lem2  10432  isf32lem11  10441  isf33lem  10444  domtriomlem  10520  axdc3  10532  zorn2lem7  10580  zorn2g  10581  fpwwe2cbv  10715  fpwwecbv  10729  pwfseq  10749  axgroth6  10913  dedekind  11473  suprleub  12283  infregelb  12301  nnsub  12382  uzwo  13038  ublbneg  13060  zsupss  13064  xrub  13442  fsuppmapnn0fiubex  14135  monoord2  14176  faclbnd4lem4  14440  bccl  14466  hashbc  14598  wrdind  14871  wrd2ind  14872  reuccatpfxs1  14896  cau3lem  15522  climmpt2  15740  caucvgrlem  15840  caurcvg2  15845  caucvgb  15847  fsum0diag2  15949  incexclem  16005  cvgrat  16052  mertenslem2  16054  mertens  16055  sqrt2irr  16417  gcdcllem1  16669  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  prmind2  16860  prmpwdvds  17082  prmreclem5  17098  prmreclem6  17099  vdwlem7  17165  vdwlem10  17168  vdwlem13  17171  vdwnn  17176  ramcl  17207  isacs2  17827  catpropd  17883  chnind  18795  chnub  18796  grpinvalem  18854  grpinva  18855  gsumvalx  18865  mndind  19024  issubg4  19356  isnsg2  19366  elnmz  19373  gsmsymgreqlem2  19645  psgnunilem5  19708  psgnunilem3  19710  efgsdm  19944  gsummptnn0fzfv  20201  pgpfac1lem5  20295  pgpfac1  20296  pgpfac  20300  ablfaclem3  20303  lbsextg  21440  evlslem2  22388  mpfind  22424  cply1mul  22614  mdetuni0  22936  m2cpminvid2lem  23072  mp2pm2mplem4  23127  chcoeffeqlem  23203  cayhamlem3  23205  elcls3  23401  isclo2  23406  neiptopnei  23450  tgcn  23570  subbascn  23572  txcmplem2  23961  kqfvima  24049  kqt0lem  24055  isr0  24056  r0cld  24057  regr1lem2  24059  fbun  24159  flftg  24315  fclsbas  24340  alexsubALTlem2  24367  alexsubALTlem4  24369  ptcmplem4  24374  tsmsxplem1  24472  tsmsxp  24474  ustuqtop  24565  utopsnneip  24567  prdsxmslem2  24848  isclmp  25418  iscau4  25600  caucfil  25604  iscmet3  25614  bcthlem5  25649  bcth  25650  ovolicc2lem5  25842  uniioombllem6  25909  vitali  25934  ismbf3d  25975  itg1climres  26035  itg2seq  26063  itg2monolem1  26071  itg2mono  26074  rolle  26310  dvlipcn  26314  dvivthlem1  26328  ply1divex  26455  fta1g  26488  dgrco  26594  plydivex  26618  fta1  26629  vieta1  26635  ulmcaulem  26721  ulmcau  26722  abelthlem8  26766  wilth  27398  fta  27407  fsumdvdsmul  27522  dchrelbas3  27565  2sqlem6  27750  2sqlem10  27755  dchrisumlem3  27818  dchrisum  27819  dchrmusumlema  27820  dchrvmasumlema  27827  dchrisum0lema  27841  pntibndlem3  27919  pntlem3  27936  pntleml  27938  pnt3  27939  ostth2lem2  27961  ostth  27966  nosupcbv  28059  nosupdm  28061  nosupbnd1lem4  28068  nosupbnd2  28073  noinfcbv  28074  noinfdm  28076  noinfres  28079  noinfbnd1lem1  28080  noinfbnd2  28088  madebdayim  28274  madebday  28286  cofss  28316  coiniss  28317  cutminmax  28322  precsexlem9  28601  onsfi  28742  n0subs  28749  bdayfinbndcbv  28852  bdayfinbndlem2  28854  z12zsodd  28868  axcontlem1  29542  axcontlem6  29547  uspgr2wlkeq  30226  crctcshwlkn0  30410  frgrwopreglem5ALT  30923  grpoideu  31111  ubthlem3  31474  adjsym  32435  lnopunilem1  32612  elunop2  32615  lnophm  32621  cnlnadjlem5  32673  mdbr3  32899  mdbr4  32900  dmdbr3  32907  dmdbr4  32908  mddmd2  32911  fprodex01  33416  prodindf  33429  wrdt2ind  33516  toslublem  33533  tosglblem  33535  archiabl  33759  isarchiofld  33760  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem4  33806  elrgspnsubrunlem2  33809  1arithidom  34069  1arithufdlem3  34078  vietadeg1  34210  vieta  34212  fedgmul  34263  fldextrspunlsplem  34305  constrconj  34377  qtophaus  34468  lmdvg  34585  esumcvg  34718  unelldsys  34791  ldgenpisyslem1  34796  eulerpartlemsv3  34993  eulerpartlemgvv  35008  signstfvneq0  35201  reprinfz1  35251  tgoldbachgtd  35291  bnj1185  35423  bnj222  35513  bnj517  35515  bnj1452  35682  bnj1463  35685  werankwe  35739  derangenlem  35936  subfacp1lem6  35950  subfacp1  35951  resconn  36011  cvmscbv  36023  sat1el2xp  36144  untangtr  36479  dfon2lem3  36547  dfon2lem7  36551  nadddilem2  36970  nadddilem4  36972  nn0prpwlem  37110  neibastop3  37150  fnemeet2  37155  weiunlem  37251  mh-infprim2bi  37335  mh-infprim3bi  37336  fvineqsnf1  38333  fvineqsneu  38334  pibt2  38340  phpreu  38527  poimirlem27  38565  heicant  38573  mblfinlem2  38576  ovoliunnfl  38580  voliunnfl  38582  mbfresfi  38584  upixp  38663  sdclem2  38676  fdc  38679  mettrifi  38691  heiborlem5  38749  heiborlem10  38754  heibor  38755  bfp  38758  disjressuc2  39343  cdleme25cv  41415  cdleme40v  41526  aks4d1p7  43133  aks6d1c1p3  43160  aks6d1c1p4  43161  supinf  43293  fsuppind  43618  mzpclval  43735  dford3lem1  44032  aomclem3  44057  aomclem4  44058  aomclem8  44062  dfac11  44063  hbtlem5  44129  nadd1suc  44393  ntrk2imkb  45036  ntrclsk2  45067  ntrclsk4  45071  fnchoice  46045  cncmpmax  46048  wessf1ornlem  46199  disjinfi  46206  rnmptbdd  46256  rnmptbd2  46260  rnmptbd  46267  supxrunb3  46409  unb2ltle  46424  monoord2xrv  46492  uzubioo2  46578  mccl  46609  climsuse  46619  limsupre  46650  limsuppnf  46720  limsupubuz  46722  limsupmnf  46730  limsupre2  46734  limsupmnfuz  46736  limsupre2mpt  46739  limsupre3  46742  limsupre3mpt  46743  limsupre3uzlem  46744  limsupre3uz  46745  limsupreuz  46746  limsupvaluz2  46747  limsupreuzmpt  46748  climuz  46753  lmbr3  46756  limsupge  46770  liminflelimsup  46785  liminfreuz  46812  xlimpnfxnegmnf  46823  cnrefiisp  46839  xlimmnf  46850  xlimpnf  46851  xlimmnfmpt  46852  xlimpnfmpt  46853  dfxlim2  46857  dvbdfbdioolem2  46938  dvbdfbdioo  46939  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem3  46957  stoweidlem7  47016  stoweidlem15  47024  stoweidlem35  47044  wallispilem3  47076  fourierdlem68  47183  fourierdlem71  47186  fourierdlem73  47188  fourierdlem87  47202  fourierdlem100  47215  fourierdlem103  47218  fourierdlem104  47219  fourierdlem107  47222  fourierdlem109  47224  fourierdlem112  47227  etransc  47292  qndenserrnbllem  47303  dfsalgen2  47350  subsaliuncl  47367  meaiuninclem  47489  ovnsubaddlem2  47580  hoidmvlelem5  47608  hoidmvle  47609  hoiqssbllem3  47633  vonioo  47691  vonicc  47694  issmf  47737  issmfle  47754  issmfgt  47765  issmfge  47779  smfsuplem2  47821  chnerlem1  47891  tmachlem-agreesn  47956  2reuimp0  48183  uniimafveqt  48462  sbgoldbm  48881  mogoldbb  48882  bgoldbtbndlem4  48905  bgoldbtbnd  48906  nn0sumshdiglem1  49732  ipolub  50095  ipoglb  50098