Theorem cbvralvw 3245

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3355 with a disjoint variable condition, which does not require ax-10 2179, ax-11 2195, ax-12 2216, ax-13 2406. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2406. (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 2848	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2069	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3082	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3082	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-ral 3082

This theorem is used by:  cbvraldva  3247  cbvral2vw  3249  cbvral3vw  3251  cbvral4vw  3252  reu7  3697  cbviinv  5006  disjxun  5109  reusv3i  5377  wereu2  5660  cnvpo  6292  frpomin  6345  f1mpt  7264  dfwe2  7779  tfinds  7862  frrlem1  8289  tfrlem1  8368  tfrlem12  8382  rdglem1  8408  tz7.48lem  8434  cbvixpv  8919  nneneq  9197  marypha1lem  9400  supub  9426  suplub  9427  ordtypecbv  9486  ordtypelem3  9489  ordtypelem9  9495  wemaplem1  9515  brwdom3  9551  ttrclss  9696  ttrclselem2  9702  tcrank  9863  infxpenc2  10022  aceq1  10117  aceq2  10119  dfac5  10128  dfac9  10136  dfac12lem3  10145  kmlem12  10161  kmlem14  10163  cofsmo  10268  infpssrlem4  10305  isfin3ds  10328  isf32lem2  10353  isf32lem11  10362  isf33lem  10365  domtriomlem  10441  axdc3  10453  zorn2lem7  10501  zorn2g  10502  fpwwe2cbv  10632  fpwwecbv  10646  pwfseq  10666  axgroth6  10830  dedekind  11390  suprleub  12198  infregelb  12216  nnsub  12297  uzwo  12953  ublbneg  12975  zsupss  12979  xrub  13356  fsuppmapnn0fiubex  14048  monoord2  14089  faclbnd4lem4  14352  bccl  14378  hashbc  14510  wrdind  14783  wrd2ind  14784  reuccatpfxs1  14808  cau3lem  15432  climmpt2  15650  caucvgrlem  15750  caurcvg2  15755  caucvgb  15757  fsum0diag2  15859  incexclem  15915  cvgrat  15962  mertenslem2  15964  mertens  15965  sqrt2irr  16329  gcdcllem1  16581  lcmfunsnlem1  16719  lcmfunsnlem2lem1  16720  prmind2  16767  prmpwdvds  16988  prmreclem5  17004  prmreclem6  17005  vdwlem7  17071  vdwlem10  17074  vdwlem13  17077  vdwnn  17082  ramcl  17113  isacs2  17733  catpropd  17789  chnind  18701  chnub  18702  grpinvalem  18759  grpinva  18760  gsumvalx  18768  mndind  18926  issubg4  19258  isnsg2  19268  elnmz  19275  gsmsymgreqlem2  19547  psgnunilem5  19610  psgnunilem3  19612  efgsdm  19846  gsummptnn0fzfv  20103  pgpfac1lem5  20197  pgpfac1  20198  pgpfac  20202  ablfaclem3  20205  lbsextg  21338  evlslem2  22282  mpfind  22318  cply1mul  22508  mdetuni0  22830  m2cpminvid2lem  22963  mp2pm2mplem4  23018  chcoeffeqlem  23094  cayhamlem3  23096  elcls3  23292  isclo2  23297  neiptopnei  23341  tgcn  23461  subbascn  23463  txcmplem2  23852  kqfvima  23940  kqt0lem  23946  isr0  23947  r0cld  23948  regr1lem2  23950  fbun  24050  flftg  24206  fclsbas  24231  alexsubALTlem2  24258  alexsubALTlem4  24260  ptcmplem4  24265  tsmsxplem1  24363  tsmsxp  24365  ustuqtop  24456  utopsnneip  24458  prdsxmslem2  24739  isclmp  25309  iscau4  25491  caucfil  25495  iscmet3  25505  bcthlem5  25540  bcth  25541  ovolicc2lem5  25733  uniioombllem6  25800  vitali  25825  ismbf3d  25866  itg1climres  25926  itg2seq  25954  itg2monolem1  25962  itg2mono  25965  rolle  26202  dvlipcn  26206  dvivthlem1  26220  ply1divex  26347  fta1g  26380  dgrco  26485  plydivex  26511  fta1  26522  vieta1  26526  ulmcaulem  26610  ulmcau  26611  abelthlem8  26655  wilth  27288  fta  27297  fsumdvdsmul  27412  dchrelbas3  27455  2sqlem6  27640  2sqlem10  27645  dchrisumlem3  27708  dchrisum  27709  dchrmusumlema  27710  dchrvmasumlema  27717  dchrisum0lema  27731  pntibndlem3  27809  pntlem3  27826  pntleml  27828  pnt3  27829  ostth2lem2  27851  ostth  27856  nosupcbv  27919  nosupdm  27921  nosupbnd1lem4  27928  nosupbnd2  27933  noinfcbv  27934  noinfdm  27936  noinfres  27939  noinfbnd1lem1  27940  noinfbnd2  27948  madebdayim  28134  madebday  28146  cofss  28176  coiniss  28177  cutminmax  28182  precsexlem9  28461  onsfi  28602  n0subs  28609  bdayfinbndcbv  28712  bdayfinbndlem2  28714  z12zsodd  28728  axcontlem1  29371  axcontlem6  29376  uspgr2wlkeq  30055  crctcshwlkn0  30239  frgrwopreglem5ALT  30746  grpoideu  30934  ubthlem3  31297  adjsym  32258  lnopunilem1  32435  elunop2  32438  lnophm  32444  cnlnadjlem5  32496  mdbr3  32722  mdbr4  32723  dmdbr3  32730  dmdbr4  32731  mddmd2  32734  fprodex01  33241  prodindf  33254  wrdt2ind  33341  toslublem  33358  tosglblem  33360  archiabl  33584  isarchiofld  33585  elrgspnlem1  33628  elrgspnlem2  33629  elrgspnlem4  33631  elrgspnsubrunlem2  33634  1arithidom  33893  1arithufdlem3  33902  vietadeg1  34034  vieta  34036  fedgmul  34087  fldextrspunlsplem  34129  constrconj  34201  qtophaus  34292  lmdvg  34409  esumcvg  34542  unelldsys  34615  ldgenpisyslem1  34620  eulerpartlemsv3  34818  eulerpartlemgvv  34833  signstfvneq0  35026  reprinfz1  35076  tgoldbachgtd  35116  bnj1185  35248  bnj222  35338  bnj517  35340  bnj1452  35507  bnj1463  35510  derangenlem  35702  subfacp1lem6  35716  subfacp1  35717  resconn  35777  cvmscbv  35789  sat1el2xp  35910  untangtr  36245  dfon2lem3  36314  dfon2lem7  36318  nadddilem2  36752  nadddilem4  36754  nn0prpwlem  36892  neibastop3  36932  fnemeet2  36937  weiunlem  37033  mh-infprim2bi  37117  mh-infprim3bi  37118  fvineqsnf1  38115  fvineqsneu  38116  pibt2  38122  phpreu  38314  poimirlem27  38357  heicant  38365  mblfinlem2  38368  ovoliunnfl  38372  voliunnfl  38374  mbfresfi  38376  upixp  38440  sdclem2  38453  fdc  38456  mettrifi  38468  heiborlem5  38526  heiborlem10  38531  heibor  38532  bfp  38535  disjressuc2  39120  cdleme25cv  41192  cdleme40v  41303  aks4d1p7  42910  aks6d1c1p3  42937  aks6d1c1p4  42938  supinf  43070  fsuppind  43382  mzpclval  43516  dford3lem1  43813  fnwe2lem1  43837  aomclem3  43843  aomclem4  43844  aomclem8  43848  dfac11  43849  hbtlem5  43915  nadd1suc  44179  ntrk2imkb  44823  ntrclsk2  44854  ntrclsk4  44858  fnchoice  45809  cncmpmax  45812  wessf1ornlem  45963  disjinfi  45970  rnmptbdd  46020  rnmptbd2  46024  rnmptbd  46031  supxrunb3  46174  unb2ltle  46189  monoord2xrv  46257  uzubioo2  46343  mccl  46374  climsuse  46384  limsupre  46415  limsuppnf  46485  limsupubuz  46487  limsupmnf  46495  limsupre2  46499  limsupmnfuz  46501  limsupre2mpt  46504  limsupre3  46507  limsupre3mpt  46508  limsupre3uzlem  46509  limsupre3uz  46510  limsupreuz  46511  limsupvaluz2  46512  limsupreuzmpt  46513  climuz  46518  lmbr3  46521  limsupge  46535  liminflelimsup  46550  liminfreuz  46577  xlimpnfxnegmnf  46588  cnrefiisp  46604  xlimmnf  46615  xlimpnf  46616  xlimmnfmpt  46617  xlimpnfmpt  46618  dfxlim2  46622  dvbdfbdioolem2  46703  dvbdfbdioo  46704  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnprodlem3  46722  stoweidlem7  46781  stoweidlem15  46789  stoweidlem35  46809  wallispilem3  46841  fourierdlem68  46948  fourierdlem71  46951  fourierdlem73  46953  fourierdlem87  46967  fourierdlem100  46980  fourierdlem103  46983  fourierdlem104  46984  fourierdlem107  46987  fourierdlem109  46989  fourierdlem112  46992  etransc  47057  qndenserrnbllem  47068  dfsalgen2  47115  subsaliuncl  47132  meaiuninclem  47254  ovnsubaddlem2  47345  hoidmvlelem5  47373  hoidmvle  47374  hoiqssbllem3  47398  vonioo  47456  vonicc  47459  issmf  47502  issmfle  47519  issmfgt  47530  issmfge  47544  smfsuplem2  47586  chnerlem1  47658  2reuimp0  47911  uniimafveqt  48190  sbgoldbm  48609  mogoldbb  48610  bgoldbtbndlem4  48633  bgoldbtbnd  48634  nn0sumshdiglem1  49460  ipolub  49825  ipoglb  49828