Theorem cbvralvw 3372

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3377 with a disjoint variable condition, which does not require ax-10 2139, ax-11 2156, ax-12 2173, ax-13 2372. (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 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2040	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3068	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817  df-ral 3068

This theorem is referenced by:  cbvral2vw  3385  cbvral3vw  3387  reu7  3662  disjxun  5068  reusv3i  5322  wereu2  5577  cnvpo  6179  frpomin  6228  f1mpt  7115  dfwe2  7602  tfinds  7681  frrlem1  8073  wfrlem1OLD  8110  tfrlem1  8178  tfrlem12  8191  rdglem1  8217  tz7.48lem  8242  nneneq  8896  marypha1lem  9122  supub  9148  suplub  9149  ordtypecbv  9206  ordtypelem3  9209  ordtypelem9  9215  wemaplem1  9235  brwdom3  9271  tcrank  9573  infxpenc2  9709  aceq1  9804  aceq2  9806  dfac5  9815  dfac9  9823  dfac12lem3  9832  kmlem12  9848  kmlem14  9850  cofsmo  9956  infpssrlem4  9993  isfin3ds  10016  isf32lem2  10041  isf32lem11  10050  isf33lem  10053  domtriomlem  10129  axdc3  10141  zorn2lem7  10189  zorn2g  10190  fpwwe2cbv  10317  fpwwecbv  10331  pwfseq  10351  axgroth6  10515  dedekind  11068  suprleub  11871  infregelb  11889  nnsub  11947  uzwo  12580  ublbneg  12602  zsupss  12606  xrub  12975  fsuppmapnn0fiubex  13640  monoord2  13682  faclbnd4lem4  13938  bccl  13964  hashbc  14093  wrdind  14363  wrd2ind  14364  reuccatpfxs1  14388  cau3lem  14994  climmpt2  15210  caucvgrlem  15312  caurcvg2  15317  caucvgb  15319  fsum0diag2  15423  incexclem  15476  cvgrat  15523  mertenslem2  15525  mertens  15526  sqrt2irr  15886  gcdcllem1  16134  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  prmind2  16318  prmpwdvds  16533  prmreclem5  16549  prmreclem6  16550  vdwlem7  16616  vdwlem10  16619  vdwlem13  16622  vdwnn  16627  ramcl  16658  isacs2  17279  catpropd  17335  grprinvlem  18272  grprinvd  18273  gsumvalx  18275  mndind  18381  issubg4  18689  isnsg2  18699  elnmz  18706  gsmsymgreqlem2  18954  psgnunilem5  19017  psgnunilem3  19019  efgsdm  19251  gsummptnn0fzfv  19503  pgpfac1lem5  19597  pgpfac1  19598  pgpfac  19602  ablfaclem3  19605  lbsextg  20339  evlslem2  21199  mpfind  21227  cply1mul  21375  mdetuni0  21678  m2cpminvid2lem  21811  mp2pm2mplem4  21866  chcoeffeqlem  21942  cayhamlem3  21944  elcls3  22142  isclo2  22147  neiptopnei  22191  tgcn  22311  subbascn  22313  txcmplem2  22701  kqfvima  22789  kqt0lem  22795  isr0  22796  r0cld  22797  regr1lem2  22799  fbun  22899  flftg  23055  fclsbas  23080  alexsubALTlem2  23107  alexsubALTlem4  23109  ptcmplem4  23114  tsmsxplem1  23212  tsmsxp  23214  ustuqtop  23306  utopsnneip  23308  prdsxmslem2  23591  isclmp  24166  iscau4  24348  caucfil  24352  iscmet3  24362  bcthlem5  24397  bcth  24398  ovolicc2lem5  24590  uniioombllem6  24657  vitali  24682  ismbf3d  24723  itg1climres  24784  itg2seq  24812  itg2monolem1  24820  itg2mono  24823  rolle  25059  dvlipcn  25063  dvivthlem1  25077  ply1divex  25206  fta1g  25237  dgrco  25341  plydivex  25362  fta1  25373  vieta1  25377  ulmcaulem  25458  ulmcau  25459  abelthlem8  25503  wilth  26125  fta  26134  dchrelbas3  26291  2sqlem6  26476  2sqlem10  26481  dchrisumlem3  26544  dchrisum  26545  dchrmusumlema  26546  dchrvmasumlema  26553  dchrisum0lema  26567  pntibndlem3  26645  pntlem3  26662  pntleml  26664  pnt3  26665  ostth2lem2  26687  ostth  26692  axcontlem1  27235  axcontlem6  27240  uspgr2wlkeq  27915  crctcshwlkn0  28087  frgrwopreglem5ALT  28587  grpoideu  28772  ubthlem3  29135  adjsym  30096  lnopunilem1  30273  elunop2  30276  lnophm  30282  cnlnadjlem5  30334  mdbr3  30560  mdbr4  30561  dmdbr3  30568  dmdbr4  30569  mddmd2  30572  fprodex01  31041  wrdt2ind  31127  toslublem  31152  tosglblem  31154  archiabl  31354  isarchiofld  31418  fedgmul  31614  qtophaus  31688  lmdvg  31805  prodindf  31891  esumcvg  31954  unelldsys  32026  ldgenpisyslem1  32031  eulerpartlemsv3  32228  eulerpartlemgvv  32243  signstfvneq0  32451  reprinfz1  32502  tgoldbachgtd  32542  bnj1185  32673  bnj222  32763  bnj517  32765  bnj1452  32932  bnj1463  32935  derangenlem  33033  subfacp1lem6  33047  subfacp1  33048  resconn  33108  cvmscbv  33120  sat1el2xp  33241  untangtr  33555  dfon2lem3  33667  dfon2lem7  33671  ttrclss  33706  ttrclselem2  33712  nosupcbv  33832  nosupdm  33834  nosupbnd1lem4  33841  nosupbnd2  33846  noinfcbv  33847  noinfdm  33849  noinfres  33852  noinfbnd1lem1  33853  noinfbnd2  33861  madebdayim  33997  madebday  34007  nn0prpwlem  34438  neibastop3  34478  fnemeet2  34483  fvineqsnf1  35508  fvineqsneu  35509  pibt2  35515  phpreu  35688  poimirlem27  35731  heicant  35739  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  mbfresfi  35750  upixp  35814  sdclem2  35827  fdc  35830  mettrifi  35842  heiborlem5  35900  heiborlem10  35905  heibor  35906  bfp  35909  cdleme25cv  38299  cdleme40v  38410  aks4d1p7  40019  fsuppind  40202  mzpclval  40463  dford3lem1  40764  fnwe2lem1  40791  aomclem3  40797  aomclem4  40798  aomclem8  40802  dfac11  40803  hbtlem5  40869  ntrk2imkb  41536  ntrclsk2  41567  ntrclsk4  41571  fnchoice  42461  cncmpmax  42464  wessf1ornlem  42611  disjinfi  42620  rnmptbdd  42679  rnmptbd2  42684  rnmptbd  42691  supxrunb3  42829  unb2ltle  42845  monoord2xrv  42914  uzubioo2  42997  mccl  43029  climsuse  43039  limsupre  43072  limsuppnf  43142  limsupubuz  43144  limsupmnf  43152  limsupre2  43156  limsupmnfuz  43158  limsupre2mpt  43161  limsupre3  43164  limsupre3mpt  43165  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  limsupvaluz2  43169  limsupreuzmpt  43170  climuz  43175  lmbr3  43178  limsupge  43192  liminflelimsup  43207  liminfreuz  43234  xlimpnfxnegmnf  43245  cnrefiisp  43261  xlimmnf  43272  xlimpnf  43273  xlimmnfmpt  43274  xlimpnfmpt  43275  dfxlim2  43279  dvbdfbdioolem2  43360  dvbdfbdioo  43361  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem3  43379  stoweidlem7  43438  stoweidlem15  43446  stoweidlem35  43466  wallispilem3  43498  fourierdlem68  43605  fourierdlem71  43608  fourierdlem73  43610  fourierdlem87  43624  fourierdlem100  43637  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem109  43646  fourierdlem112  43649  etransc  43714  qndenserrnbllem  43725  dfsalgen2  43770  subsaliuncl  43787  meaiuninclem  43908  ovnsubaddlem2  43999  hoidmvlelem5  44027  hoidmvle  44028  hoiqssbllem3  44052  vonioo  44110  vonicc  44113  issmf  44151  issmfle  44168  issmfgt  44179  issmfge  44192  smfsuplem2  44232  2reuimp0  44493  uniimafveqt  44721  sbgoldbm  45124  mogoldbb  45125  bgoldbtbndlem4  45148  bgoldbtbnd  45149  nn0sumshdiglem1  45855  ipolub  46162  ipoglb  46165