Theorem cbvralvw 3396

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3399 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2175, ax-13 2379. (Contributed by NM, 28-Jan-1997.) (Revised by Gino Giotto, 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 2872	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 348	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2043	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3111	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2870  df-ral 3111

This theorem is referenced by:  cbvral2vw  3408  cbvral3vw  3410  reu7  3671  disjxun  5028  reusv3i  5270  wereu2  5516  cnvpo  6106  f1mpt  6997  dfwe2  7476  tfinds  7554  wfrlem1  7937  tfrlem1  7995  tfrlem12  8008  rdglem1  8034  tz7.48lem  8060  nneneq  8684  marypha1lem  8881  supub  8907  suplub  8908  ordtypecbv  8965  ordtypelem3  8968  ordtypelem9  8974  wemaplem1  8994  brwdom3  9030  tcrank  9297  infxpenc2  9433  aceq1  9528  aceq2  9530  dfac5  9539  dfac9  9547  dfac12lem3  9556  kmlem12  9572  kmlem14  9574  cofsmo  9680  infpssrlem4  9717  isfin3ds  9740  isf32lem2  9765  isf32lem11  9774  isf33lem  9777  domtriomlem  9853  axdc3  9865  zorn2lem7  9913  zorn2g  9914  fpwwe2cbv  10041  fpwwecbv  10055  pwfseq  10075  axgroth6  10239  dedekind  10792  suprleub  11594  infregelb  11612  nnsub  11669  uzwo  12299  ublbneg  12321  zsupss  12325  xrub  12693  fsuppmapnn0fiubex  13355  monoord2  13397  faclbnd4lem4  13652  bccl  13678  hashbc  13807  wrdind  14075  wrd2ind  14076  reuccatpfxs1  14100  cau3lem  14706  climmpt2  14922  caucvgrlem  15021  caurcvg2  15026  caucvgb  15028  fsum0diag2  15130  incexclem  15183  cvgrat  15231  mertenslem2  15233  mertens  15234  sqrt2irr  15594  gcdcllem1  15838  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  prmind2  16019  prmpwdvds  16230  prmreclem5  16246  prmreclem6  16247  vdwlem7  16313  vdwlem10  16316  vdwlem13  16319  vdwnn  16324  ramcl  16355  isacs2  16916  catpropd  16971  grprinvlem  17875  grprinvd  17876  gsumvalx  17878  mndind  17984  issubg4  18290  isnsg2  18300  elnmz  18307  gsmsymgreqlem2  18551  psgnunilem5  18614  psgnunilem3  18616  efgsdm  18848  gsummptnn0fzfv  19100  pgpfac1lem5  19194  pgpfac1  19195  pgpfac  19199  ablfaclem3  19202  lbsextg  19927  evlslem2  20751  mpfind  20779  cply1mul  20923  mdetuni0  21226  m2cpminvid2lem  21359  mp2pm2mplem4  21414  chcoeffeqlem  21490  cayhamlem3  21492  elcls3  21688  isclo2  21693  neiptopnei  21737  tgcn  21857  subbascn  21859  txcmplem2  22247  kqfvima  22335  kqt0lem  22341  isr0  22342  r0cld  22343  regr1lem2  22345  fbun  22445  flftg  22601  fclsbas  22626  alexsubALTlem2  22653  alexsubALTlem4  22655  ptcmplem4  22660  tsmsxplem1  22758  tsmsxp  22760  ustuqtop  22852  utopsnneip  22854  prdsxmslem2  23136  isclmp  23702  iscau4  23883  caucfil  23887  iscmet3  23897  bcthlem5  23932  bcth  23933  ovolicc2lem5  24125  uniioombllem6  24192  vitali  24217  ismbf3d  24258  itg1climres  24318  itg2seq  24346  itg2monolem1  24354  itg2mono  24357  rolle  24593  dvlipcn  24597  dvivthlem1  24611  ply1divex  24737  fta1g  24768  dgrco  24872  plydivex  24893  fta1  24904  vieta1  24908  ulmcaulem  24989  ulmcau  24990  abelthlem8  25034  wilth  25656  fta  25665  dchrelbas3  25822  2sqlem6  26007  2sqlem10  26012  dchrisumlem3  26075  dchrisum  26076  dchrmusumlema  26077  dchrvmasumlema  26084  dchrisum0lema  26098  pntibndlem3  26176  pntlem3  26193  pntleml  26195  pnt3  26196  ostth2lem2  26218  ostth  26223  axcontlem1  26758  axcontlem6  26763  uspgr2wlkeq  27435  crctcshwlkn0  27607  frgrwopreglem5ALT  28107  grpoideu  28292  ubthlem3  28655  adjsym  29616  lnopunilem1  29793  elunop2  29796  lnophm  29802  cnlnadjlem5  29854  mdbr3  30080  mdbr4  30081  dmdbr3  30088  dmdbr4  30089  mddmd2  30092  fprodex01  30567  wrdt2ind  30653  toslublem  30680  tosglblem  30682  archiabl  30877  isarchiofld  30941  fedgmul  31115  qtophaus  31189  lmdvg  31306  prodindf  31392  esumcvg  31455  unelldsys  31527  ldgenpisyslem1  31532  eulerpartlemsv3  31729  eulerpartlemgvv  31744  signstfvneq0  31952  reprinfz1  32003  tgoldbachgtd  32043  bnj1185  32175  bnj222  32265  bnj517  32267  bnj1452  32434  bnj1463  32437  derangenlem  32531  subfacp1lem6  32545  subfacp1  32546  resconn  32606  cvmscbv  32618  sat1el2xp  32739  untangtr  33053  dfon2lem3  33143  dfon2lem7  33147  frpomin  33191  frrlem1  33236  nosupdm  33317  nosupbnd1lem4  33324  nosupbnd2  33329  nn0prpwlem  33783  neibastop3  33823  fnemeet2  33828  fvineqsnf1  34827  fvineqsneu  34828  pibt2  34834  phpreu  35041  poimirlem27  35084  heicant  35092  mblfinlem2  35095  ovoliunnfl  35099  voliunnfl  35101  mbfresfi  35103  upixp  35167  sdclem2  35180  fdc  35183  mettrifi  35195  heiborlem5  35253  heiborlem10  35258  heibor  35259  bfp  35262  cdleme25cv  37654  cdleme40v  37765  fsuppind  39456  mzpclval  39666  dford3lem1  39967  fnwe2lem1  39994  aomclem3  40000  aomclem4  40001  aomclem8  40005  dfac11  40006  hbtlem5  40072  ntrk2imkb  40740  ntrclsk2  40771  ntrclsk4  40775  fnchoice  41658  cncmpmax  41661  wessf1ornlem  41811  disjinfi  41820  rnmptbdd  41882  rnmptbd2  41887  rnmptbd  41894  supxrunb3  42036  unb2ltle  42052  monoord2xrv  42123  uzubioo2  42206  mccl  42240  climsuse  42250  limsupre  42283  limsuppnf  42353  limsupubuz  42355  limsupmnf  42363  limsupre2  42367  limsupmnfuz  42369  limsupre2mpt  42372  limsupre3  42375  limsupre3mpt  42376  limsupre3uzlem  42377  limsupre3uz  42378  limsupreuz  42379  limsupvaluz2  42380  limsupreuzmpt  42381  climuz  42386  lmbr3  42389  limsupge  42403  liminflelimsup  42418  liminfreuz  42445  xlimpnfxnegmnf  42456  cnrefiisp  42472  xlimmnf  42483  xlimpnf  42484  xlimmnfmpt  42485  xlimpnfmpt  42486  dfxlim2  42490  dvbdfbdioolem2  42571  dvbdfbdioo  42572  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnprodlem3  42590  stoweidlem7  42649  stoweidlem15  42657  stoweidlem35  42677  wallispilem3  42709  fourierdlem68  42816  fourierdlem71  42819  fourierdlem73  42821  fourierdlem87  42835  fourierdlem100  42848  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  fourierdlem109  42857  fourierdlem112  42860  etransc  42925  qndenserrnbllem  42936  dfsalgen2  42981  subsaliuncl  42998  meaiuninclem  43119  ovnsubaddlem2  43210  hoidmvlelem5  43238  hoidmvle  43239  hoiqssbllem3  43263  vonioo  43321  vonicc  43324  issmf  43362  issmfle  43379  issmfgt  43390  issmfge  43403  smfsuplem2  43443  2reuimp0  43670  uniimafveqt  43898  sbgoldbm  44302  mogoldbb  44303  bgoldbtbndlem4  44326  bgoldbtbnd  44327  nn0sumshdiglem1  45035