Theorem cbvralvw 3216

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3336 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  3692  cbviinv  4997  disjxun  5098  reusv3i  5351  wereu2  5629  cnvpo  6253  frpomin  6306  f1mpt  7217  dfwe2  7729  tfinds  7812  frrlem1  8238  tfrlem1  8317  tfrlem12  8330  rdglem1  8356  tz7.48lem  8382  cbvixpv  8865  nneneq  9142  marypha1lem  9348  supub  9374  suplub  9375  ordtypecbv  9434  ordtypelem3  9437  ordtypelem9  9443  wemaplem1  9463  brwdom3  9499  ttrclss  9641  ttrclselem2  9647  tcrank  9808  infxpenc2  9944  aceq1  10039  aceq2  10041  dfac5  10051  dfac9  10059  dfac12lem3  10068  kmlem12  10084  kmlem14  10086  cofsmo  10191  infpssrlem4  10228  isfin3ds  10251  isf32lem2  10276  isf32lem11  10285  isf33lem  10288  domtriomlem  10364  axdc3  10376  zorn2lem7  10424  zorn2g  10425  fpwwe2cbv  10553  fpwwecbv  10567  pwfseq  10587  axgroth6  10751  dedekind  11308  suprleub  12120  infregelb  12138  nnsub  12201  uzwo  12836  ublbneg  12858  zsupss  12862  xrub  13239  fsuppmapnn0fiubex  13927  monoord2  13968  faclbnd4lem4  14231  bccl  14257  hashbc  14388  wrdind  14657  wrd2ind  14658  reuccatpfxs1  14682  cau3lem  15290  climmpt2  15508  caucvgrlem  15608  caurcvg2  15613  caucvgb  15615  fsum0diag2  15718  incexclem  15771  cvgrat  15818  mertenslem2  15820  mertens  15821  sqrt2irr  16186  gcdcllem1  16438  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  prmind2  16624  prmpwdvds  16844  prmreclem5  16860  prmreclem6  16861  vdwlem7  16927  vdwlem10  16930  vdwlem13  16933  vdwnn  16938  ramcl  16969  isacs2  17588  catpropd  17644  chnind  18556  chnub  18557  grpinvalem  18610  grpinva  18611  gsumvalx  18613  mndind  18765  issubg4  19090  isnsg2  19100  elnmz  19107  gsmsymgreqlem2  19375  psgnunilem5  19438  psgnunilem3  19440  efgsdm  19674  gsummptnn0fzfv  19931  pgpfac1lem5  20025  pgpfac1  20026  pgpfac  20030  ablfaclem3  20033  lbsextg  21132  evlslem2  22049  mpfind  22085  cply1mul  22255  mdetuni0  22580  m2cpminvid2lem  22713  mp2pm2mplem4  22768  chcoeffeqlem  22844  cayhamlem3  22846  elcls3  23042  isclo2  23047  neiptopnei  23091  tgcn  23211  subbascn  23213  txcmplem2  23601  kqfvima  23689  kqt0lem  23695  isr0  23696  r0cld  23697  regr1lem2  23699  fbun  23799  flftg  23955  fclsbas  23980  alexsubALTlem2  24007  alexsubALTlem4  24009  ptcmplem4  24014  tsmsxplem1  24112  tsmsxp  24114  ustuqtop  24205  utopsnneip  24207  prdsxmslem2  24488  isclmp  25068  iscau4  25250  caucfil  25254  iscmet3  25264  bcthlem5  25299  bcth  25300  ovolicc2lem5  25493  uniioombllem6  25560  vitali  25585  ismbf3d  25626  itg1climres  25686  itg2seq  25714  itg2monolem1  25722  itg2mono  25725  rolle  25965  dvlipcn  25970  dvivthlem1  25984  ply1divex  26113  fta1g  26146  dgrco  26252  plydivex  26276  fta1  26287  vieta1  26291  ulmcaulem  26374  ulmcau  26375  abelthlem8  26420  wilth  27052  fta  27061  fsumdvdsmul  27176  dchrelbas3  27220  2sqlem6  27405  2sqlem10  27410  dchrisumlem3  27473  dchrisum  27474  dchrmusumlema  27475  dchrvmasumlema  27482  dchrisum0lema  27496  pntibndlem3  27574  pntlem3  27591  pntleml  27593  pnt3  27594  ostth2lem2  27616  ostth  27621  nosupcbv  27685  nosupdm  27687  nosupbnd1lem4  27694  nosupbnd2  27699  noinfcbv  27700  noinfdm  27702  noinfres  27705  noinfbnd1lem1  27706  noinfbnd2  27714  madebdayim  27899  madebday  27911  cofss  27941  coiniss  27942  cutminmax  27947  precsexlem9  28226  onsfi  28367  n0subs  28374  bdayfinbndcbv  28477  bdayfinbndlem2  28479  z12zsodd  28493  axcontlem1  29053  axcontlem6  29058  uspgr2wlkeq  29735  crctcshwlkn0  29910  frgrwopreglem5ALT  30413  grpoideu  30601  ubthlem3  30964  adjsym  31925  lnopunilem1  32102  elunop2  32105  lnophm  32111  cnlnadjlem5  32163  mdbr3  32389  mdbr4  32390  dmdbr3  32397  dmdbr4  32398  mddmd2  32401  fprodex01  32921  prodindf  32959  wrdt2ind  33050  toslublem  33069  tosglblem  33071  archiabl  33296  isarchiofld  33297  elrgspnlem1  33340  elrgspnlem2  33341  elrgspnlem4  33343  elrgspnsubrunlem2  33346  1arithidom  33634  1arithufdlem3  33643  vietadeg1  33759  vieta  33761  fedgmul  33813  fldextrspunlsplem  33855  constrconj  33927  qtophaus  34018  lmdvg  34135  esumcvg  34268  unelldsys  34340  ldgenpisyslem1  34345  eulerpartlemsv3  34543  eulerpartlemgvv  34558  signstfvneq0  34754  reprinfz1  34804  tgoldbachgtd  34844  bnj1185  34973  bnj222  35063  bnj517  35065  bnj1452  35232  bnj1463  35235  derangenlem  35391  subfacp1lem6  35405  subfacp1  35406  resconn  35466  cvmscbv  35478  sat1el2xp  35599  untangtr  35934  dfon2lem3  36003  dfon2lem7  36007  nn0prpwlem  36542  neibastop3  36582  fnemeet2  36587  weiunlem  36683  fvineqsnf1  37669  fvineqsneu  37670  pibt2  37676  phpreu  37859  poimirlem27  37902  heicant  37910  mblfinlem2  37913  ovoliunnfl  37917  voliunnfl  37919  mbfresfi  37921  upixp  37984  sdclem2  37997  fdc  38000  mettrifi  38012  heiborlem5  38070  heiborlem10  38075  heibor  38076  bfp  38079  disjressuc2  38666  cdleme25cv  40738  cdleme40v  40849  aks4d1p7  42457  aks6d1c1p3  42484  aks6d1c1p4  42485  supinf  42616  fsuppind  42952  mzpclval  43086  dford3lem1  43387  fnwe2lem1  43411  aomclem3  43417  aomclem4  43418  aomclem8  43422  dfac11  43423  hbtlem5  43489  nadd1suc  43753  ntrk2imkb  44397  ntrclsk2  44428  ntrclsk4  44432  fnchoice  45393  cncmpmax  45396  wessf1ornlem  45548  disjinfi  45555  rnmptbdd  45607  rnmptbd2  45611  rnmptbd  45618  supxrunb3  45761  unb2ltle  45777  monoord2xrv  45845  uzubioo2  45931  mccl  45962  climsuse  45972  limsupre  46003  limsuppnf  46073  limsupubuz  46075  limsupmnf  46083  limsupre2  46087  limsupmnfuz  46089  limsupre2mpt  46092  limsupre3  46095  limsupre3mpt  46096  limsupre3uzlem  46097  limsupre3uz  46098  limsupreuz  46099  limsupvaluz2  46100  limsupreuzmpt  46101  climuz  46106  lmbr3  46109  limsupge  46123  liminflelimsup  46138  liminfreuz  46165  xlimpnfxnegmnf  46176  cnrefiisp  46192  xlimmnf  46203  xlimpnf  46204  xlimmnfmpt  46205  xlimpnfmpt  46206  dfxlim2  46210  dvbdfbdioolem2  46291  dvbdfbdioo  46292  ioodvbdlimc1lem1  46293  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  dvnprodlem3  46310  stoweidlem7  46369  stoweidlem15  46377  stoweidlem35  46397  wallispilem3  46429  fourierdlem68  46536  fourierdlem71  46539  fourierdlem73  46541  fourierdlem87  46555  fourierdlem100  46568  fourierdlem103  46571  fourierdlem104  46572  fourierdlem107  46575  fourierdlem109  46577  fourierdlem112  46580  etransc  46645  qndenserrnbllem  46656  dfsalgen2  46703  subsaliuncl  46720  meaiuninclem  46842  ovnsubaddlem2  46933  hoidmvlelem5  46961  hoidmvle  46962  hoiqssbllem3  46986  vonioo  47044  vonicc  47047  issmf  47090  issmfle  47107  issmfgt  47118  issmfge  47132  smfsuplem2  47174  chnerlem1  47244  2reuimp0  47478  uniimafveqt  47745  sbgoldbm  48148  mogoldbb  48149  bgoldbtbndlem4  48172  bgoldbtbnd  48173  nn0sumshdiglem1  48985  ipolub  49351  ipoglb  49354