Theorem cbvralvw 3216

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3340 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2178, ax-13 2371. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2371. (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 2812	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2036	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3046	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3046	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ral 3046

This theorem is referenced by:  cbvraldva  3218  cbvral2vw  3220  cbvral3vw  3222  cbvral4vw  3223  reu7  3706  cbviinv  5008  disjxun  5108  reusv3i  5362  wereu2  5638  cnvpo  6263  frpomin  6316  f1mpt  7239  dfwe2  7753  tfinds  7839  frrlem1  8268  tfrlem1  8347  tfrlem12  8360  rdglem1  8386  tz7.48lem  8412  cbvixpv  8891  nneneq  9176  marypha1lem  9391  supub  9417  suplub  9418  ordtypecbv  9477  ordtypelem3  9480  ordtypelem9  9486  wemaplem1  9506  brwdom3  9542  ttrclss  9680  ttrclselem2  9686  tcrank  9844  infxpenc2  9982  aceq1  10077  aceq2  10079  dfac5  10089  dfac9  10097  dfac12lem3  10106  kmlem12  10122  kmlem14  10124  cofsmo  10229  infpssrlem4  10266  isfin3ds  10289  isf32lem2  10314  isf32lem11  10323  isf33lem  10326  domtriomlem  10402  axdc3  10414  zorn2lem7  10462  zorn2g  10463  fpwwe2cbv  10590  fpwwecbv  10604  pwfseq  10624  axgroth6  10788  dedekind  11344  suprleub  12156  infregelb  12174  nnsub  12237  uzwo  12877  ublbneg  12899  zsupss  12903  xrub  13279  fsuppmapnn0fiubex  13964  monoord2  14005  faclbnd4lem4  14268  bccl  14294  hashbc  14425  wrdind  14694  wrd2ind  14695  reuccatpfxs1  14719  cau3lem  15328  climmpt2  15546  caucvgrlem  15646  caurcvg2  15651  caucvgb  15653  fsum0diag2  15756  incexclem  15809  cvgrat  15856  mertenslem2  15858  mertens  15859  sqrt2irr  16224  gcdcllem1  16476  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  prmind2  16662  prmpwdvds  16882  prmreclem5  16898  prmreclem6  16899  vdwlem7  16965  vdwlem10  16968  vdwlem13  16971  vdwnn  16976  ramcl  17007  isacs2  17621  catpropd  17677  grpinvalem  18607  grpinva  18608  gsumvalx  18610  mndind  18762  issubg4  19084  isnsg2  19095  elnmz  19102  gsmsymgreqlem2  19368  psgnunilem5  19431  psgnunilem3  19433  efgsdm  19667  gsummptnn0fzfv  19924  pgpfac1lem5  20018  pgpfac1  20019  pgpfac  20023  ablfaclem3  20026  lbsextg  21079  evlslem2  21993  mpfind  22021  cply1mul  22190  mdetuni0  22515  m2cpminvid2lem  22648  mp2pm2mplem4  22703  chcoeffeqlem  22779  cayhamlem3  22781  elcls3  22977  isclo2  22982  neiptopnei  23026  tgcn  23146  subbascn  23148  txcmplem2  23536  kqfvima  23624  kqt0lem  23630  isr0  23631  r0cld  23632  regr1lem2  23634  fbun  23734  flftg  23890  fclsbas  23915  alexsubALTlem2  23942  alexsubALTlem4  23944  ptcmplem4  23949  tsmsxplem1  24047  tsmsxp  24049  ustuqtop  24141  utopsnneip  24143  prdsxmslem2  24424  isclmp  25004  iscau4  25186  caucfil  25190  iscmet3  25200  bcthlem5  25235  bcth  25236  ovolicc2lem5  25429  uniioombllem6  25496  vitali  25521  ismbf3d  25562  itg1climres  25622  itg2seq  25650  itg2monolem1  25658  itg2mono  25661  rolle  25901  dvlipcn  25906  dvivthlem1  25920  ply1divex  26049  fta1g  26082  dgrco  26188  plydivex  26212  fta1  26223  vieta1  26227  ulmcaulem  26310  ulmcau  26311  abelthlem8  26356  wilth  26988  fta  26997  fsumdvdsmul  27112  dchrelbas3  27156  2sqlem6  27341  2sqlem10  27346  dchrisumlem3  27409  dchrisum  27410  dchrmusumlema  27411  dchrvmasumlema  27418  dchrisum0lema  27432  pntibndlem3  27510  pntlem3  27527  pntleml  27529  pnt3  27530  ostth2lem2  27552  ostth  27557  nosupcbv  27621  nosupdm  27623  nosupbnd1lem4  27630  nosupbnd2  27635  noinfcbv  27636  noinfdm  27638  noinfres  27641  noinfbnd1lem1  27642  noinfbnd2  27650  madebdayim  27806  madebday  27818  cofss  27845  coiniss  27846  precsexlem9  28124  onsfi  28254  n0subs  28260  zs12bday  28350  axcontlem1  28898  axcontlem6  28903  uspgr2wlkeq  29581  crctcshwlkn0  29758  frgrwopreglem5ALT  30258  grpoideu  30445  ubthlem3  30808  adjsym  31769  lnopunilem1  31946  elunop2  31949  lnophm  31955  cnlnadjlem5  32007  mdbr3  32233  mdbr4  32234  dmdbr3  32241  dmdbr4  32242  mddmd2  32245  fprodex01  32757  prodindf  32793  wrdt2ind  32882  toslublem  32905  tosglblem  32907  chnind  32944  chnub  32945  archiabl  33159  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  isarchiofld  33302  1arithidom  33515  1arithufdlem3  33524  fedgmul  33634  fldextrspunlsplem  33675  constrconj  33742  qtophaus  33833  lmdvg  33950  esumcvg  34083  unelldsys  34155  ldgenpisyslem1  34160  eulerpartlemsv3  34359  eulerpartlemgvv  34374  signstfvneq0  34570  reprinfz1  34620  tgoldbachgtd  34660  bnj1185  34790  bnj222  34880  bnj517  34882  bnj1452  35049  bnj1463  35052  derangenlem  35165  subfacp1lem6  35179  subfacp1  35180  resconn  35240  cvmscbv  35252  sat1el2xp  35373  untangtr  35708  dfon2lem3  35780  dfon2lem7  35784  nn0prpwlem  36317  neibastop3  36357  fnemeet2  36362  weiunlem2  36458  fvineqsnf1  37405  fvineqsneu  37406  pibt2  37412  phpreu  37605  poimirlem27  37648  heicant  37656  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  mbfresfi  37667  upixp  37730  sdclem2  37743  fdc  37746  mettrifi  37758  heiborlem5  37816  heiborlem10  37821  heibor  37822  bfp  37825  disjressuc2  38381  cdleme25cv  40359  cdleme40v  40470  aks4d1p7  42078  aks6d1c1p3  42105  aks6d1c1p4  42106  supinf  42237  fsuppind  42585  mzpclval  42720  dford3lem1  43022  fnwe2lem1  43046  aomclem3  43052  aomclem4  43053  aomclem8  43057  dfac11  43058  hbtlem5  43124  nadd1suc  43388  ntrk2imkb  44033  ntrclsk2  44064  ntrclsk4  44068  fnchoice  45030  cncmpmax  45033  wessf1ornlem  45186  disjinfi  45193  rnmptbdd  45246  rnmptbd2  45250  rnmptbd  45257  supxrunb3  45402  unb2ltle  45418  monoord2xrv  45486  uzubioo2  45572  mccl  45603  climsuse  45613  limsupre  45646  limsuppnf  45716  limsupubuz  45718  limsupmnf  45726  limsupre2  45730  limsupmnfuz  45732  limsupre2mpt  45735  limsupre3  45738  limsupre3mpt  45739  limsupre3uzlem  45740  limsupre3uz  45741  limsupreuz  45742  limsupvaluz2  45743  limsupreuzmpt  45744  climuz  45749  lmbr3  45752  limsupge  45766  liminflelimsup  45781  liminfreuz  45808  xlimpnfxnegmnf  45819  cnrefiisp  45835  xlimmnf  45846  xlimpnf  45847  xlimmnfmpt  45848  xlimpnfmpt  45849  dfxlim2  45853  dvbdfbdioolem2  45934  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem3  45953  stoweidlem7  46012  stoweidlem15  46020  stoweidlem35  46040  wallispilem3  46072  fourierdlem68  46179  fourierdlem71  46182  fourierdlem73  46184  fourierdlem87  46198  fourierdlem100  46211  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  fourierdlem112  46223  etransc  46288  qndenserrnbllem  46299  dfsalgen2  46346  subsaliuncl  46363  meaiuninclem  46485  ovnsubaddlem2  46576  hoidmvlelem5  46604  hoidmvle  46605  hoiqssbllem3  46629  vonioo  46687  vonicc  46690  issmf  46733  issmfle  46750  issmfgt  46761  issmfge  46775  smfsuplem2  46817  2reuimp0  47119  uniimafveqt  47386  sbgoldbm  47789  mogoldbb  47790  bgoldbtbndlem4  47813  bgoldbtbnd  47814  nn0sumshdiglem1  48614  ipolub  48980  ipoglb  48983