Theorem cbvralvw 3240

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

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

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 2147

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

This theorem is used by:  cbvraldva  3242  cbvral2vw  3244  cbvral3vw  3246  cbvral4vw  3247  reu7  3690  cbviinv  4998  disjxun  5101  reusv3i  5369  wereu2  5652  cnvpo  6285  frpomin  6338  f1mpt  7259  dfwe2  7774  tfinds  7857  frrlem1  8286  tfrlem1  8365  tfrlem12  8379  rdglem1  8405  tz7.48lemOLD  8433  cbvixpv  8925  nneneq  9203  marypha1lem  9406  supub  9432  suplub  9433  ordtypecbv  9492  ordtypelem3  9495  ordtypelem9  9501  wemaplem1  9521  brwdom3  9557  ttrclss  9702  ttrclselem2  9708  tcrank  9869  infxpenc2  10028  aceq1  10123  aceq2  10125  dfac5  10134  dfac9  10142  dfac12lem3  10151  kmlem12  10167  kmlem14  10169  cofsmo  10274  infpssrlem4  10311  isfin3ds  10334  isf32lem2  10359  isf32lem11  10368  isf33lem  10371  domtriomlem  10447  axdc3  10459  zorn2lem7  10507  zorn2g  10508  fpwwe2cbv  10642  fpwwecbv  10656  pwfseq  10676  axgroth6  10840  dedekind  11400  suprleub  12208  infregelb  12226  nnsub  12307  uzwo  12963  ublbneg  12985  zsupss  12989  xrub  13367  fsuppmapnn0fiubex  14059  monoord2  14100  faclbnd4lem4  14363  bccl  14389  hashbc  14521  wrdind  14794  wrd2ind  14795  reuccatpfxs1  14819  cau3lem  15445  climmpt2  15663  caucvgrlem  15763  caurcvg2  15768  caucvgb  15770  fsum0diag2  15872  incexclem  15928  cvgrat  15975  mertenslem2  15977  mertens  15978  sqrt2irr  16340  gcdcllem1  16592  lcmfunsnlem1  16730  lcmfunsnlem2lem1  16731  prmind2  16778  prmpwdvds  16999  prmreclem5  17015  prmreclem6  17016  vdwlem7  17082  vdwlem10  17085  vdwlem13  17088  vdwnn  17093  ramcl  17124  isacs2  17744  catpropd  17800  chnind  18712  chnub  18713  grpinvalem  18770  grpinva  18771  gsumvalx  18781  mndind  18940  issubg4  19272  isnsg2  19282  elnmz  19289  gsmsymgreqlem2  19561  psgnunilem5  19624  psgnunilem3  19626  efgsdm  19860  gsummptnn0fzfv  20117  pgpfac1lem5  20211  pgpfac1  20212  pgpfac  20216  ablfaclem3  20219  lbsextg  21352  evlslem2  22298  mpfind  22334  cply1mul  22524  mdetuni0  22846  m2cpminvid2lem  22982  mp2pm2mplem4  23037  chcoeffeqlem  23113  cayhamlem3  23115  elcls3  23311  isclo2  23316  neiptopnei  23360  tgcn  23480  subbascn  23482  txcmplem2  23871  kqfvima  23959  kqt0lem  23965  isr0  23966  r0cld  23967  regr1lem2  23969  fbun  24069  flftg  24225  fclsbas  24250  alexsubALTlem2  24277  alexsubALTlem4  24279  ptcmplem4  24284  tsmsxplem1  24382  tsmsxp  24384  ustuqtop  24475  utopsnneip  24477  prdsxmslem2  24758  isclmp  25328  iscau4  25510  caucfil  25514  iscmet3  25524  bcthlem5  25559  bcth  25560  ovolicc2lem5  25752  uniioombllem6  25819  vitali  25844  ismbf3d  25885  itg1climres  25945  itg2seq  25973  itg2monolem1  25981  itg2mono  25984  rolle  26220  dvlipcn  26224  dvivthlem1  26238  ply1divex  26365  fta1g  26398  dgrco  26504  plydivex  26530  fta1  26541  vieta1  26547  ulmcaulem  26633  ulmcau  26634  abelthlem8  26678  wilth  27310  fta  27319  fsumdvdsmul  27434  dchrelbas3  27477  2sqlem6  27662  2sqlem10  27667  dchrisumlem3  27730  dchrisum  27731  dchrmusumlema  27732  dchrvmasumlema  27739  dchrisum0lema  27753  pntibndlem3  27831  pntlem3  27848  pntleml  27850  pnt3  27851  ostth2lem2  27873  ostth  27878  nosupcbv  27941  nosupdm  27943  nosupbnd1lem4  27950  nosupbnd2  27955  noinfcbv  27956  noinfdm  27958  noinfres  27961  noinfbnd1lem1  27962  noinfbnd2  27970  madebdayim  28156  madebday  28168  cofss  28198  coiniss  28199  cutminmax  28204  precsexlem9  28483  onsfi  28624  n0subs  28631  bdayfinbndcbv  28734  bdayfinbndlem2  28736  z12zsodd  28750  axcontlem1  29424  axcontlem6  29429  uspgr2wlkeq  30108  crctcshwlkn0  30292  frgrwopreglem5ALT  30805  grpoideu  30993  ubthlem3  31356  adjsym  32317  lnopunilem1  32494  elunop2  32497  lnophm  32503  cnlnadjlem5  32555  mdbr3  32781  mdbr4  32782  dmdbr3  32789  dmdbr4  32790  mddmd2  32793  fprodex01  33298  prodindf  33311  wrdt2ind  33398  toslublem  33415  tosglblem  33417  archiabl  33641  isarchiofld  33642  elrgspnlem1  33685  elrgspnlem2  33686  elrgspnlem4  33688  elrgspnsubrunlem2  33691  1arithidom  33950  1arithufdlem3  33959  vietadeg1  34091  vieta  34093  fedgmul  34144  fldextrspunlsplem  34186  constrconj  34258  qtophaus  34349  lmdvg  34466  esumcvg  34599  unelldsys  34672  ldgenpisyslem1  34677  eulerpartlemsv3  34875  eulerpartlemgvv  34890  signstfvneq0  35083  reprinfz1  35133  tgoldbachgtd  35173  bnj1185  35305  bnj222  35395  bnj517  35397  bnj1452  35564  bnj1463  35567  derangenlem  35753  subfacp1lem6  35767  subfacp1  35768  resconn  35828  cvmscbv  35840  sat1el2xp  35961  untangtr  36296  dfon2lem3  36365  dfon2lem7  36369  nadddilem2  36804  nadddilem4  36806  nn0prpwlem  36944  neibastop3  36984  fnemeet2  36989  weiunlem  37085  mh-infprim2bi  37169  mh-infprim3bi  37170  fvineqsnf1  38167  fvineqsneu  38168  pibt2  38174  phpreu  38361  poimirlem27  38399  heicant  38407  mblfinlem2  38410  ovoliunnfl  38414  voliunnfl  38416  mbfresfi  38418  upixp  38482  sdclem2  38495  fdc  38498  mettrifi  38510  heiborlem5  38568  heiborlem10  38573  heibor  38574  bfp  38577  disjressuc2  39162  cdleme25cv  41234  cdleme40v  41345  aks4d1p7  42952  aks6d1c1p3  42979  aks6d1c1p4  42980  supinf  43112  fsuppind  43439  mzpclval  43573  dford3lem1  43870  fnwe2lem1  43894  aomclem3  43900  aomclem4  43901  aomclem8  43905  dfac11  43906  hbtlem5  43972  nadd1suc  44236  ntrk2imkb  44880  ntrclsk2  44911  ntrclsk4  44915  fnchoice  45866  cncmpmax  45869  wessf1ornlem  46020  disjinfi  46027  rnmptbdd  46077  rnmptbd2  46081  rnmptbd  46088  supxrunb3  46231  unb2ltle  46246  monoord2xrv  46314  uzubioo2  46400  mccl  46431  climsuse  46441  limsupre  46472  limsuppnf  46542  limsupubuz  46544  limsupmnf  46552  limsupre2  46556  limsupmnfuz  46558  limsupre2mpt  46561  limsupre3  46564  limsupre3mpt  46565  limsupre3uzlem  46566  limsupre3uz  46567  limsupreuz  46568  limsupvaluz2  46569  limsupreuzmpt  46570  climuz  46575  lmbr3  46578  limsupge  46592  liminflelimsup  46607  liminfreuz  46634  xlimpnfxnegmnf  46645  cnrefiisp  46661  xlimmnf  46672  xlimpnf  46673  xlimmnfmpt  46674  xlimpnfmpt  46675  dfxlim2  46679  dvbdfbdioolem2  46760  dvbdfbdioo  46761  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnprodlem3  46779  stoweidlem7  46838  stoweidlem15  46846  stoweidlem35  46866  wallispilem3  46898  fourierdlem68  47005  fourierdlem71  47008  fourierdlem73  47010  fourierdlem87  47024  fourierdlem100  47037  fourierdlem103  47040  fourierdlem104  47041  fourierdlem107  47044  fourierdlem109  47046  fourierdlem112  47049  etransc  47114  qndenserrnbllem  47125  dfsalgen2  47172  subsaliuncl  47189  meaiuninclem  47311  ovnsubaddlem2  47402  hoidmvlelem5  47430  hoidmvle  47431  hoiqssbllem3  47455  vonioo  47513  vonicc  47516  issmf  47559  issmfle  47576  issmfgt  47587  issmfge  47601  smfsuplem2  47643  chnerlem1  47713  tmachlem-agreesn  47778  2reuimp0  48005  uniimafveqt  48284  sbgoldbm  48703  mogoldbb  48704  bgoldbtbndlem4  48727  bgoldbtbnd  48728  nn0sumshdiglem1  49554  ipolub  49917  ipoglb  49920