Theorem cbvralv 2765

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 1574	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2761	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  cbvral2v  2778  cbvral3v  2780  reu7  2999  reusv3i  4554  omsinds  4718  cnvpom  5277  f1mpt  5907  tfrlem1  6469  tfrlemiubacc  6491  tfrlemi1  6493  tfr1onlemubacc  6507  tfr1onlemaccex  6509  tfrcllembxssdm  6517  tfrcllemubacc  6520  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  rdgon  6547  frecfcllem  6565  frecsuclem  6567  nneneq  7038  fimax2gtrilemstep  7083  supubti  7189  suplubti  7190  finomni  7330  nninfwlporlemd  7362  nninfinfwlpo  7370  acfun  7412  exmidontriimlem3  7428  exmidontriimlem4  7429  exmidontriim  7430  ccfunen  7473  cc2  7476  cauappcvgprlemladdrl  7867  caucvgprlemcl  7886  caucvgprlemladdrl  7888  caucvgsrlembound  8004  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  suplocsrlem  8018  peano5nnnn  8102  axcaucvglemres  8109  axpre-suploc  8112  suprleubex  9124  nnsub  9172  supinfneg  9819  infsupneg  9820  infregelbex  9822  ublbneg  9837  zsupssdc  10488  exbtwnzlemex  10499  uzsinds  10696  iseqovex  10710  seq3val  10712  seqvalcd  10713  seqf  10716  seqovcd  10719  monoord2  10738  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seq3f1olemqsum  10765  seq3f1olemp  10767  seq3f1oleml  10768  seq3f1o  10769  nn0ltexp2  10961  bccl  11019  seq3shft  11389  caucvgre  11532  cvg1nlemcau  11535  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  cau3lem  11665  zsumdc  11935  fsum3  11938  isumz  11940  isumss2  11944  fsumsersdc  11946  fsum3ser  11948  fisum0diag2  11998  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratz  12083  mertenslem2  12087  mertensabs  12088  zproddc  12130  fprodseq  12134  prod1dc  12137  fprodsplitdc  12147  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemeu  12568  bezoutlemle  12569  dfgcd3  12571  prmind2  12682  sqrt2irr  12724  hashdvds  12783  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemr  13034  ctinfom  13039  ctinf  13041  ctiunctlemudc  13048  ssnnctlemct  13057  nninfdclemp1  13061  mplsubgfilemcl  14703  tgcn  14922  mulcncflem  15321  suplociccreex  15338  dedekindicc  15347  vtxedgfi  16095  vtxlpfi  16096  nnsf  16543  nninfsellemqall  16553  nninfomni  16557  trirec0  16584  apdiff  16588  iswomni0  16591  dceqnconst  16600  dcapnconst  16601  neap0mkv  16609  ltlenmkv  16610