Theorem cbvralvw 3220

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  ∀wral 3051

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 2007  ax-8 2110

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

This theorem is referenced by:  cbvraldva  3222  cbvral2vw  3224  cbvral3vw  3226  cbvral4vw  3227  reu7  3715  cbviinv  5017  disjxun  5117  reusv3i  5374  wereu2  5651  cnvpo  6276  frpomin  6329  f1mpt  7253  dfwe2  7766  tfinds  7853  frrlem1  8283  wfrlem1OLD  8320  tfrlem1  8388  tfrlem12  8401  rdglem1  8427  tz7.48lem  8453  cbvixpv  8927  nneneq  9218  marypha1lem  9443  supub  9469  suplub  9470  ordtypecbv  9529  ordtypelem3  9532  ordtypelem9  9538  wemaplem1  9558  brwdom3  9594  ttrclss  9732  ttrclselem2  9738  tcrank  9896  infxpenc2  10034  aceq1  10129  aceq2  10131  dfac5  10141  dfac9  10149  dfac12lem3  10158  kmlem12  10174  kmlem14  10176  cofsmo  10281  infpssrlem4  10318  isfin3ds  10341  isf32lem2  10366  isf32lem11  10375  isf33lem  10378  domtriomlem  10454  axdc3  10466  zorn2lem7  10514  zorn2g  10515  fpwwe2cbv  10642  fpwwecbv  10656  pwfseq  10676  axgroth6  10840  dedekind  11396  suprleub  12206  infregelb  12224  nnsub  12282  uzwo  12925  ublbneg  12947  zsupss  12951  xrub  13326  fsuppmapnn0fiubex  14008  monoord2  14049  faclbnd4lem4  14312  bccl  14338  hashbc  14469  wrdind  14738  wrd2ind  14739  reuccatpfxs1  14763  cau3lem  15371  climmpt2  15587  caucvgrlem  15687  caurcvg2  15692  caucvgb  15694  fsum0diag2  15797  incexclem  15850  cvgrat  15897  mertenslem2  15899  mertens  15900  sqrt2irr  16265  gcdcllem1  16516  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  prmind2  16702  prmpwdvds  16922  prmreclem5  16938  prmreclem6  16939  vdwlem7  17005  vdwlem10  17008  vdwlem13  17011  vdwnn  17016  ramcl  17047  isacs2  17663  catpropd  17719  grpinvalem  18649  grpinva  18650  gsumvalx  18652  mndind  18804  issubg4  19126  isnsg2  19137  elnmz  19144  gsmsymgreqlem2  19410  psgnunilem5  19473  psgnunilem3  19475  efgsdm  19709  gsummptnn0fzfv  19966  pgpfac1lem5  20060  pgpfac1  20061  pgpfac  20065  ablfaclem3  20068  lbsextg  21121  evlslem2  22035  mpfind  22063  cply1mul  22232  mdetuni0  22557  m2cpminvid2lem  22690  mp2pm2mplem4  22745  chcoeffeqlem  22821  cayhamlem3  22823  elcls3  23019  isclo2  23024  neiptopnei  23068  tgcn  23188  subbascn  23190  txcmplem2  23578  kqfvima  23666  kqt0lem  23672  isr0  23673  r0cld  23674  regr1lem2  23676  fbun  23776  flftg  23932  fclsbas  23957  alexsubALTlem2  23984  alexsubALTlem4  23986  ptcmplem4  23991  tsmsxplem1  24089  tsmsxp  24091  ustuqtop  24183  utopsnneip  24185  prdsxmslem2  24466  isclmp  25046  iscau4  25229  caucfil  25233  iscmet3  25243  bcthlem5  25278  bcth  25279  ovolicc2lem5  25472  uniioombllem6  25539  vitali  25564  ismbf3d  25605  itg1climres  25665  itg2seq  25693  itg2monolem1  25701  itg2mono  25704  rolle  25944  dvlipcn  25949  dvivthlem1  25963  ply1divex  26092  fta1g  26125  dgrco  26231  plydivex  26255  fta1  26266  vieta1  26270  ulmcaulem  26353  ulmcau  26354  abelthlem8  26399  wilth  27031  fta  27040  fsumdvdsmul  27155  dchrelbas3  27199  2sqlem6  27384  2sqlem10  27389  dchrisumlem3  27452  dchrisum  27453  dchrmusumlema  27454  dchrvmasumlema  27461  dchrisum0lema  27475  pntibndlem3  27553  pntlem3  27570  pntleml  27572  pnt3  27573  ostth2lem2  27595  ostth  27600  nosupcbv  27664  nosupdm  27666  nosupbnd1lem4  27673  nosupbnd2  27678  noinfcbv  27679  noinfdm  27681  noinfres  27684  noinfbnd1lem1  27685  noinfbnd2  27693  madebdayim  27843  madebday  27855  cofss  27881  coiniss  27882  precsexlem9  28156  n0subs  28277  zs12bday  28341  axcontlem1  28889  axcontlem6  28894  uspgr2wlkeq  29572  crctcshwlkn0  29749  frgrwopreglem5ALT  30249  grpoideu  30436  ubthlem3  30799  adjsym  31760  lnopunilem1  31937  elunop2  31940  lnophm  31946  cnlnadjlem5  31998  mdbr3  32224  mdbr4  32225  dmdbr3  32232  dmdbr4  32233  mddmd2  32236  fprodex01  32750  prodindf  32786  wrdt2ind  32875  toslublem  32898  tosglblem  32900  chnind  32937  chnub  32938  archiabl  33142  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  isarchiofld  33285  1arithidom  33498  1arithufdlem3  33507  fedgmul  33617  fldextrspunlsplem  33660  constrconj  33725  qtophaus  33813  lmdvg  33930  esumcvg  34063  unelldsys  34135  ldgenpisyslem1  34140  eulerpartlemsv3  34339  eulerpartlemgvv  34354  signstfvneq0  34550  reprinfz1  34600  tgoldbachgtd  34640  bnj1185  34770  bnj222  34860  bnj517  34862  bnj1452  35029  bnj1463  35032  derangenlem  35139  subfacp1lem6  35153  subfacp1  35154  resconn  35214  cvmscbv  35226  sat1el2xp  35347  untangtr  35677  dfon2lem3  35749  dfon2lem7  35753  nn0prpwlem  36286  neibastop3  36326  fnemeet2  36331  weiunlem2  36427  fvineqsnf1  37374  fvineqsneu  37375  pibt2  37381  phpreu  37574  poimirlem27  37617  heicant  37625  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  mbfresfi  37636  upixp  37699  sdclem2  37712  fdc  37715  mettrifi  37727  heiborlem5  37785  heiborlem10  37790  heibor  37791  bfp  37794  disjressuc2  38352  cdleme25cv  40323  cdleme40v  40434  aks4d1p7  42042  aks6d1c1p3  42069  aks6d1c1p4  42070  supinf  42240  fsuppind  42560  mzpclval  42695  dford3lem1  42997  fnwe2lem1  43021  aomclem3  43027  aomclem4  43028  aomclem8  43032  dfac11  43033  hbtlem5  43099  nadd1suc  43363  ntrk2imkb  44008  ntrclsk2  44039  ntrclsk4  44043  fnchoice  45001  cncmpmax  45004  wessf1ornlem  45157  disjinfi  45164  rnmptbdd  45217  rnmptbd2  45221  rnmptbd  45228  supxrunb3  45374  unb2ltle  45390  monoord2xrv  45458  uzubioo2  45544  mccl  45575  climsuse  45585  limsupre  45618  limsuppnf  45688  limsupubuz  45690  limsupmnf  45698  limsupre2  45702  limsupmnfuz  45704  limsupre2mpt  45707  limsupre3  45710  limsupre3mpt  45711  limsupre3uzlem  45712  limsupre3uz  45713  limsupreuz  45714  limsupvaluz2  45715  limsupreuzmpt  45716  climuz  45721  lmbr3  45724  limsupge  45738  liminflelimsup  45753  liminfreuz  45780  xlimpnfxnegmnf  45791  cnrefiisp  45807  xlimmnf  45818  xlimpnf  45819  xlimmnfmpt  45820  xlimpnfmpt  45821  dfxlim2  45825  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  stoweidlem7  45984  stoweidlem15  45992  stoweidlem35  46012  wallispilem3  46044  fourierdlem68  46151  fourierdlem71  46154  fourierdlem73  46156  fourierdlem87  46170  fourierdlem100  46183  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem109  46192  fourierdlem112  46195  etransc  46260  qndenserrnbllem  46271  dfsalgen2  46318  subsaliuncl  46335  meaiuninclem  46457  ovnsubaddlem2  46548  hoidmvlelem5  46576  hoidmvle  46577  hoiqssbllem3  46601  vonioo  46659  vonicc  46662  issmf  46705  issmfle  46722  issmfgt  46733  issmfge  46747  smfsuplem2  46789  2reuimp0  47091  uniimafveqt  47343  sbgoldbm  47746  mogoldbb  47747  bgoldbtbndlem4  47770  bgoldbtbnd  47771  nn0sumshdiglem1  48549  ipolub  48910  ipoglb  48913