Theorem cbvralvw 3449

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3452 with a disjoint variable condition, which does not require ax-10 2145, ax-11 2161, ax-12 2177, ax-13 2390. (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 2895	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2043	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3143	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3143	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893  df-ral 3143

This theorem is referenced by:  cbvral2vw  3461  cbvral3vw  3463  reu7  3723  disjxun  5064  reusv3i  5305  wereu2  5552  cnvpo  6138  f1mpt  7019  dfwe2  7496  tfinds  7574  wfrlem1  7954  tfrlem1  8012  tfrlem12  8025  rdglem1  8051  tz7.48lem  8077  nneneq  8700  marypha1lem  8897  supub  8923  suplub  8924  ordtypecbv  8981  ordtypelem3  8984  ordtypelem9  8990  wemaplem1  9010  brwdom3  9046  tcrank  9313  infxpenc2  9448  aceq1  9543  aceq2  9545  dfac5  9554  dfac9  9562  dfac12lem3  9571  kmlem12  9587  kmlem14  9589  cofsmo  9691  infpssrlem4  9728  isfin3ds  9751  isf32lem2  9776  isf32lem11  9785  isf33lem  9788  domtriomlem  9864  axdc3  9876  zorn2lem7  9924  zorn2g  9925  fpwwe2cbv  10052  fpwwecbv  10066  pwfseq  10086  axgroth6  10250  dedekind  10803  suprleub  11607  infregelb  11625  nnsub  11682  uzwo  12312  ublbneg  12334  zsupss  12338  xrub  12706  fsuppmapnn0fiubex  13361  monoord2  13402  faclbnd4lem4  13657  bccl  13683  hashbc  13812  wrdind  14084  wrd2ind  14085  reuccatpfxs1  14109  cau3lem  14714  climmpt2  14930  caucvgrlem  15029  caurcvg2  15034  caucvgb  15036  fsum0diag2  15138  incexclem  15191  cvgrat  15239  mertenslem2  15241  mertens  15242  sqrt2irr  15602  gcdcllem1  15848  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  prmind2  16029  prmpwdvds  16240  prmreclem5  16256  prmreclem6  16257  vdwlem7  16323  vdwlem10  16326  vdwlem13  16329  vdwnn  16334  ramcl  16365  isacs2  16924  catpropd  16979  grprinvlem  17883  grprinvd  17884  gsumvalx  17886  mndind  17992  issubg4  18298  isnsg2  18308  elnmz  18315  gsmsymgreqlem2  18559  psgnunilem5  18622  psgnunilem3  18624  efgsdm  18856  gsummptnn0fzfv  19107  pgpfac1lem5  19201  pgpfac1  19202  pgpfac  19206  ablfaclem3  19209  lbsextg  19934  evlslem2  20292  mpfind  20320  cply1mul  20462  mdetuni0  21230  m2cpminvid2lem  21362  mp2pm2mplem4  21417  chcoeffeqlem  21493  cayhamlem3  21495  elcls3  21691  isclo2  21696  neiptopnei  21740  tgcn  21860  subbascn  21862  txcmplem2  22250  kqfvima  22338  kqt0lem  22344  isr0  22345  r0cld  22346  regr1lem2  22348  fbun  22448  flftg  22604  fclsbas  22629  alexsubALTlem2  22656  alexsubALTlem4  22658  ptcmplem4  22663  tsmsxplem1  22761  tsmsxp  22763  ustuqtop  22855  utopsnneip  22857  prdsxmslem2  23139  isclmp  23701  iscau4  23882  caucfil  23886  iscmet3  23896  bcthlem5  23931  bcth  23932  ovolicc2lem5  24122  uniioombllem6  24189  vitali  24214  ismbf3d  24255  itg1climres  24315  itg2seq  24343  itg2monolem1  24351  itg2mono  24354  rolle  24587  dvlipcn  24591  dvivthlem1  24605  ply1divex  24730  fta1g  24761  dgrco  24865  plydivex  24886  fta1  24897  vieta1  24901  ulmcaulem  24982  ulmcau  24983  abelthlem8  25027  wilth  25648  fta  25657  dchrelbas3  25814  2sqlem6  25999  2sqlem10  26004  dchrisumlem3  26067  dchrisum  26068  dchrmusumlema  26069  dchrvmasumlema  26076  dchrisum0lema  26090  pntibndlem3  26168  pntlem3  26185  pntleml  26187  pnt3  26188  ostth2lem2  26210  ostth  26215  axcontlem1  26750  axcontlem6  26755  uspgr2wlkeq  27427  crctcshwlkn0  27599  grpoideu  28286  ubthlem3  28649  adjsym  29610  lnopunilem1  29787  elunop2  29790  lnophm  29796  cnlnadjlem5  29848  mdbr3  30074  mdbr4  30075  dmdbr3  30082  dmdbr4  30083  mddmd2  30086  fprodex01  30541  wrdt2ind  30627  toslublem  30654  tosglblem  30656  archiabl  30827  isarchiofld  30890  fedgmul  31027  qtophaus  31100  lmdvg  31196  prodindf  31282  esumcvg  31345  unelldsys  31417  ldgenpisyslem1  31422  eulerpartlemsv3  31619  eulerpartlemgvv  31634  signstfvneq0  31842  reprinfz1  31893  tgoldbachgtd  31933  bnj1185  32065  bnj222  32155  bnj517  32157  bnj1452  32324  bnj1463  32327  derangenlem  32418  subfacp1lem6  32432  subfacp1  32433  resconn  32493  cvmscbv  32505  sat1el2xp  32626  untangtr  32940  dfon2lem3  33030  dfon2lem7  33034  frpomin  33078  frrlem1  33123  nosupdm  33204  nosupbnd1lem4  33211  nosupbnd2  33216  nn0prpwlem  33670  neibastop3  33710  fnemeet2  33715  fvineqsnf1  34694  fvineqsneu  34695  pibt2  34701  phpreu  34891  poimirlem27  34934  heicant  34942  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  mbfresfi  34953  upixp  35019  sdclem2  35032  fdc  35035  mettrifi  35047  heiborlem5  35108  heiborlem10  35113  heibor  35114  bfp  35117  cdleme25cv  37509  cdleme40v  37620  mzpclval  39371  dford3lem1  39672  fnwe2lem1  39699  aomclem3  39705  aomclem4  39706  aomclem8  39710  dfac11  39711  hbtlem5  39777  ntrk2imkb  40436  ntrclsk2  40467  ntrclsk4  40471  fnchoice  41335  cncmpmax  41338  wessf1ornlem  41494  disjinfi  41503  rnmptbdd  41565  rnmptbd2  41570  rnmptbd  41577  supxrunb3  41721  unb2ltle  41738  monoord2xrv  41809  uzubioo2  41894  mccl  41928  climsuse  41938  limsupre  41971  limsuppnf  42041  limsupubuz  42043  limsupmnf  42051  limsupre2  42055  limsupmnfuz  42057  limsupre2mpt  42060  limsupre3  42063  limsupre3mpt  42064  limsupre3uzlem  42065  limsupre3uz  42066  limsupreuz  42067  limsupvaluz2  42068  limsupreuzmpt  42069  climuz  42074  lmbr3  42077  limsupge  42091  liminflelimsup  42106  liminfreuz  42133  xlimpnfxnegmnf  42144  cnrefiisp  42160  xlimmnf  42171  xlimpnf  42172  xlimmnfmpt  42173  xlimpnfmpt  42174  dfxlim2  42178  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnprodlem3  42282  stoweidlem7  42341  stoweidlem15  42349  stoweidlem35  42369  wallispilem3  42401  fourierdlem68  42508  fourierdlem71  42511  fourierdlem73  42513  fourierdlem87  42527  fourierdlem100  42540  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem109  42549  fourierdlem112  42552  etransc  42617  qndenserrnbllem  42628  dfsalgen2  42673  subsaliuncl  42690  meaiuninclem  42811  ovnsubaddlem2  42902  hoidmvlelem5  42930  hoidmvle  42931  hoiqssbllem3  42955  vonioo  43013  vonicc  43016  issmf  43054  issmfle  43071  issmfgt  43082  issmfge  43095  smfsuplem2  43135  2reuimp0  43362  uniimafveqt  43590  sbgoldbm  43998  mogoldbb  43999  bgoldbtbndlem4  44022  bgoldbtbnd  44023  nn0sumshdiglem1  44730