Theorem cbvralv 2780

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527

This theorem is referenced by:  cbvral2v  2793  cbvral3v  2795  reu7  3015  reusv3i  4585  omsinds  4749  cnvpom  5310  f1mpt  5950  tfrlem1  6552  tfrlemiubacc  6574  tfrlemi1  6576  tfr1onlemubacc  6590  tfr1onlemaccex  6592  tfrcllembxssdm  6600  tfrcllemubacc  6603  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  rdgon  6630  frecfcllem  6648  frecsuclem  6650  nneneq  7124  fimax2gtrilemstep  7171  supubti  7303  suplubti  7304  finomni  7444  nninfwlporlemd  7476  nninfinfwlpo  7484  acfun  7527  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  ccfunen  7594  cc2  7597  cauappcvgprlemladdrl  7988  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgsrlembound  8125  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  suplocsrlem  8139  peano5nnnn  8223  axcaucvglemres  8230  axpre-suploc  8233  suprleubex  9245  nnsub  9293  supinfneg  9945  infsupneg  9946  infregelbex  9948  ublbneg  9963  zsupssdc  10622  exbtwnzlemex  10633  uzsinds  10830  iseqovex  10844  seq3val  10846  seqvalcd  10847  seqf  10850  seqovcd  10853  monoord2  10872  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsum  10899  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  nn0ltexp2  11096  bccl  11154  seq3shft  11548  caucvgre  11691  cvg1nlemcau  11694  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  cau3lem  11824  zsumdc  12095  fsum3  12098  isumz  12100  isumss2  12104  fsumsersdc  12106  fsum3ser  12108  fisum0diag2  12158  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratz  12243  mertenslem2  12247  mertensabs  12248  zproddc  12290  fprodseq  12294  prod1dc  12297  fprodsplitdc  12307  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemeu  12728  bezoutlemle  12729  dfgcd3  12731  prmind2  12842  sqrt2irr  12884  hashdvds  12943  ballotfilemefi  13181  ballotfilemodife  13184  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemr  13258  ctinfom  13263  ctinf  13265  ctiunctlemudc  13272  ssnnctlemct  13281  nninfdclemp1  13285  mplsubgfilemcl  14980  tgcn  15199  mulcncflem  15598  suplociccreex  15615  dedekindicc  15624  vtxedgfi  16410  vtxlpfi  16411  nnsf  16909  nninfsellemqall  16919  nninfomni  16923  repiecef  16938  trirec0  16954  apdiff  16958  iswomni0  16962  dceqnconst  16972  dcapnconst  16973  neap0mkv  16981  ltlenmkv  16982