Theorem cbvralv 2737

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralv	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralv

Step	Hyp	Ref	Expression
1		nfv 1550	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1550	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2733	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488

This theorem is referenced by:  cbvral2v  2750  cbvral3v  2752  reu7  2967  reusv3i  4504  omsinds  4668  cnvpom  5222  f1mpt  5830  tfrlem1  6384  tfrlemiubacc  6406  tfrlemi1  6408  tfr1onlemubacc  6422  tfr1onlemaccex  6424  tfrcllembxssdm  6432  tfrcllemubacc  6435  tfrcllemaccex  6437  tfrcllemres  6438  tfrcldm  6439  rdgon  6462  frecfcllem  6480  frecsuclem  6482  nneneq  6936  fimax2gtrilemstep  6979  supubti  7083  suplubti  7084  finomni  7224  nninfwlporlemd  7256  nninfinfwlpo  7264  acfun  7301  exmidontriimlem3  7317  exmidontriimlem4  7318  exmidontriim  7319  ccfunen  7358  cc2  7361  cauappcvgprlemladdrl  7752  caucvgprlemcl  7771  caucvgprlemladdrl  7773  caucvgsrlembound  7889  caucvgsrlemgt1  7890  caucvgsrlemoffres  7895  suplocsrlem  7903  peano5nnnn  7987  axcaucvglemres  7994  axpre-suploc  7997  suprleubex  9009  nnsub  9057  supinfneg  9698  infsupneg  9699  infregelbex  9701  ublbneg  9716  zsupssdc  10362  exbtwnzlemex  10373  uzsinds  10570  iseqovex  10584  seq3val  10586  seqvalcd  10587  seqf  10590  seqovcd  10593  monoord2  10612  iseqf1olemjpcl  10634  iseqf1olemqpcl  10635  seq3f1olemqsum  10639  seq3f1olemp  10641  seq3f1oleml  10642  seq3f1o  10643  nn0ltexp2  10835  bccl  10893  seq3shft  11068  caucvgre  11211  cvg1nlemcau  11214  resqrexlemglsq  11252  resqrexlemsqa  11254  resqrexlemex  11255  cau3lem  11344  zsumdc  11614  fsum3  11617  isumz  11619  isumss2  11623  fsumsersdc  11625  fsum3ser  11627  fisum0diag2  11677  cvgratnnlemnexp  11754  cvgratnnlemmn  11755  cvgratz  11762  mertenslem2  11766  mertensabs  11767  zproddc  11809  fprodseq  11813  prod1dc  11816  fprodsplitdc  11826  bezoutlemmain  12238  bezoutlemex  12241  bezoutlemzz  12242  bezoutlemeu  12247  bezoutlemle  12248  dfgcd3  12250  prmind2  12361  sqrt2irr  12403  hashdvds  12462  ennnfoneleminc  12701  ennnfonelemex  12704  ennnfonelemr  12713  ctinfom  12718  ctinf  12720  ctiunctlemudc  12727  ssnnctlemct  12736  nninfdclemp1  12740  mplsubgfilemcl  14379  tgcn  14598  mulcncflem  14997  suplociccreex  15014  dedekindicc  15023  nnsf  15806  nninfsellemqall  15816  nninfomni  15820  trirec0  15847  apdiff  15851  iswomni0  15854  dceqnconst  15863  dcapnconst  15864  neap0mkv  15872  ltlenmkv  15873