Theorem cbvralvw 3207

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3327 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2178, ax-13 2370. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2370. (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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2036	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3045	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3045	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ral 3045

This theorem is referenced by:  cbvraldva  3209  cbvral2vw  3211  cbvral3vw  3213  cbvral4vw  3214  reu7  3692  cbviinv  4990  disjxun  5090  reusv3i  5343  wereu2  5616  cnvpo  6235  frpomin  6288  f1mpt  7198  dfwe2  7710  tfinds  7793  frrlem1  8219  tfrlem1  8298  tfrlem12  8311  rdglem1  8337  tz7.48lem  8363  cbvixpv  8842  nneneq  9120  marypha1lem  9323  supub  9349  suplub  9350  ordtypecbv  9409  ordtypelem3  9412  ordtypelem9  9418  wemaplem1  9438  brwdom3  9474  ttrclss  9616  ttrclselem2  9622  tcrank  9780  infxpenc2  9916  aceq1  10011  aceq2  10013  dfac5  10023  dfac9  10031  dfac12lem3  10040  kmlem12  10056  kmlem14  10058  cofsmo  10163  infpssrlem4  10200  isfin3ds  10223  isf32lem2  10248  isf32lem11  10257  isf33lem  10260  domtriomlem  10336  axdc3  10348  zorn2lem7  10396  zorn2g  10397  fpwwe2cbv  10524  fpwwecbv  10538  pwfseq  10558  axgroth6  10722  dedekind  11279  suprleub  12091  infregelb  12109  nnsub  12172  uzwo  12812  ublbneg  12834  zsupss  12838  xrub  13214  fsuppmapnn0fiubex  13899  monoord2  13940  faclbnd4lem4  14203  bccl  14229  hashbc  14360  wrdind  14628  wrd2ind  14629  reuccatpfxs1  14653  cau3lem  15262  climmpt2  15480  caucvgrlem  15580  caurcvg2  15585  caucvgb  15587  fsum0diag2  15690  incexclem  15743  cvgrat  15790  mertenslem2  15792  mertens  15793  sqrt2irr  16158  gcdcllem1  16410  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  prmind2  16596  prmpwdvds  16816  prmreclem5  16832  prmreclem6  16833  vdwlem7  16899  vdwlem10  16902  vdwlem13  16905  vdwnn  16910  ramcl  16941  isacs2  17559  catpropd  17615  grpinvalem  18547  grpinva  18548  gsumvalx  18550  mndind  18702  issubg4  19024  isnsg2  19035  elnmz  19042  gsmsymgreqlem2  19310  psgnunilem5  19373  psgnunilem3  19375  efgsdm  19609  gsummptnn0fzfv  19866  pgpfac1lem5  19960  pgpfac1  19961  pgpfac  19965  ablfaclem3  19968  lbsextg  21069  evlslem2  21984  mpfind  22012  cply1mul  22181  mdetuni0  22506  m2cpminvid2lem  22639  mp2pm2mplem4  22694  chcoeffeqlem  22770  cayhamlem3  22772  elcls3  22968  isclo2  22973  neiptopnei  23017  tgcn  23137  subbascn  23139  txcmplem2  23527  kqfvima  23615  kqt0lem  23621  isr0  23622  r0cld  23623  regr1lem2  23625  fbun  23725  flftg  23881  fclsbas  23906  alexsubALTlem2  23933  alexsubALTlem4  23935  ptcmplem4  23940  tsmsxplem1  24038  tsmsxp  24040  ustuqtop  24132  utopsnneip  24134  prdsxmslem2  24415  isclmp  24995  iscau4  25177  caucfil  25181  iscmet3  25191  bcthlem5  25226  bcth  25227  ovolicc2lem5  25420  uniioombllem6  25487  vitali  25512  ismbf3d  25553  itg1climres  25613  itg2seq  25641  itg2monolem1  25649  itg2mono  25652  rolle  25892  dvlipcn  25897  dvivthlem1  25911  ply1divex  26040  fta1g  26073  dgrco  26179  plydivex  26203  fta1  26214  vieta1  26218  ulmcaulem  26301  ulmcau  26302  abelthlem8  26347  wilth  26979  fta  26988  fsumdvdsmul  27103  dchrelbas3  27147  2sqlem6  27332  2sqlem10  27337  dchrisumlem3  27400  dchrisum  27401  dchrmusumlema  27402  dchrvmasumlema  27409  dchrisum0lema  27423  pntibndlem3  27501  pntlem3  27518  pntleml  27520  pnt3  27521  ostth2lem2  27543  ostth  27548  nosupcbv  27612  nosupdm  27614  nosupbnd1lem4  27621  nosupbnd2  27626  noinfcbv  27627  noinfdm  27629  noinfres  27632  noinfbnd1lem1  27633  noinfbnd2  27641  madebdayim  27802  madebday  27814  cofss  27843  coiniss  27844  precsexlem9  28122  onsfi  28252  n0subs  28258  zs12zodd  28359  zs12bday  28361  axcontlem1  28909  axcontlem6  28914  uspgr2wlkeq  29591  crctcshwlkn0  29766  frgrwopreglem5ALT  30266  grpoideu  30453  ubthlem3  30816  adjsym  31777  lnopunilem1  31954  elunop2  31957  lnophm  31963  cnlnadjlem5  32015  mdbr3  32241  mdbr4  32242  dmdbr3  32249  dmdbr4  32250  mddmd2  32253  fprodex01  32771  prodindf  32807  wrdt2ind  32896  toslublem  32915  tosglblem  32917  chnind  32954  chnub  32955  archiabl  33141  isarchiofld  33142  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  1arithidom  33475  1arithufdlem3  33484  fedgmul  33604  fldextrspunlsplem  33646  constrconj  33718  qtophaus  33809  lmdvg  33926  esumcvg  34059  unelldsys  34131  ldgenpisyslem1  34136  eulerpartlemsv3  34335  eulerpartlemgvv  34350  signstfvneq0  34546  reprinfz1  34596  tgoldbachgtd  34636  bnj1185  34766  bnj222  34856  bnj517  34858  bnj1452  35025  bnj1463  35028  derangenlem  35154  subfacp1lem6  35168  subfacp1  35169  resconn  35229  cvmscbv  35241  sat1el2xp  35362  untangtr  35697  dfon2lem3  35769  dfon2lem7  35773  nn0prpwlem  36306  neibastop3  36346  fnemeet2  36351  weiunlem2  36447  fvineqsnf1  37394  fvineqsneu  37395  pibt2  37401  phpreu  37594  poimirlem27  37637  heicant  37645  mblfinlem2  37648  ovoliunnfl  37652  voliunnfl  37654  mbfresfi  37656  upixp  37719  sdclem2  37732  fdc  37735  mettrifi  37747  heiborlem5  37805  heiborlem10  37810  heibor  37811  bfp  37814  disjressuc2  38370  cdleme25cv  40347  cdleme40v  40458  aks4d1p7  42066  aks6d1c1p3  42093  aks6d1c1p4  42094  supinf  42225  fsuppind  42573  mzpclval  42708  dford3lem1  43009  fnwe2lem1  43033  aomclem3  43039  aomclem4  43040  aomclem8  43044  dfac11  43045  hbtlem5  43111  nadd1suc  43375  ntrk2imkb  44020  ntrclsk2  44051  ntrclsk4  44055  fnchoice  45017  cncmpmax  45020  wessf1ornlem  45173  disjinfi  45180  rnmptbdd  45233  rnmptbd2  45237  rnmptbd  45244  supxrunb3  45388  unb2ltle  45404  monoord2xrv  45472  uzubioo2  45558  mccl  45589  climsuse  45599  limsupre  45632  limsuppnf  45702  limsupubuz  45704  limsupmnf  45712  limsupre2  45716  limsupmnfuz  45718  limsupre2mpt  45721  limsupre3  45724  limsupre3mpt  45725  limsupre3uzlem  45726  limsupre3uz  45727  limsupreuz  45728  limsupvaluz2  45729  limsupreuzmpt  45730  climuz  45735  lmbr3  45738  limsupge  45752  liminflelimsup  45767  liminfreuz  45794  xlimpnfxnegmnf  45805  cnrefiisp  45821  xlimmnf  45832  xlimpnf  45833  xlimmnfmpt  45834  xlimpnfmpt  45835  dfxlim2  45839  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnprodlem3  45939  stoweidlem7  45998  stoweidlem15  46006  stoweidlem35  46026  wallispilem3  46058  fourierdlem68  46165  fourierdlem71  46168  fourierdlem73  46170  fourierdlem87  46184  fourierdlem100  46197  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem109  46206  fourierdlem112  46209  etransc  46274  qndenserrnbllem  46285  dfsalgen2  46332  subsaliuncl  46349  meaiuninclem  46471  ovnsubaddlem2  46562  hoidmvlelem5  46590  hoidmvle  46591  hoiqssbllem3  46615  vonioo  46673  vonicc  46676  issmf  46719  issmfle  46736  issmfgt  46747  issmfge  46761  smfsuplem2  46803  2reuimp0  47108  uniimafveqt  47375  sbgoldbm  47778  mogoldbb  47779  bgoldbtbndlem4  47802  bgoldbtbnd  47803  nn0sumshdiglem1  48616  ipolub  48982  ipoglb  48985