Theorem cbvralv 2778

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 2774	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525

This theorem is referenced by:  cbvral2v  2791  cbvral3v  2793  reu7  3012  reusv3i  4580  omsinds  4744  cnvpom  5305  f1mpt  5944  tfrlem1  6539  tfrlemiubacc  6561  tfrlemi1  6563  tfr1onlemubacc  6577  tfr1onlemaccex  6579  tfrcllembxssdm  6587  tfrcllemubacc  6590  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  rdgon  6617  frecfcllem  6635  frecsuclem  6637  nneneq  7111  fimax2gtrilemstep  7158  supubti  7290  suplubti  7291  finomni  7431  nninfwlporlemd  7463  nninfinfwlpo  7471  acfun  7514  exmidontriimlem3  7530  exmidontriimlem4  7531  exmidontriim  7532  ccfunen  7578  cc2  7581  cauappcvgprlemladdrl  7972  caucvgprlemcl  7991  caucvgprlemladdrl  7993  caucvgsrlembound  8109  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  suplocsrlem  8123  peano5nnnn  8207  axcaucvglemres  8214  axpre-suploc  8217  suprleubex  9228  nnsub  9276  supinfneg  9927  infsupneg  9928  infregelbex  9930  ublbneg  9945  zsupssdc  10598  exbtwnzlemex  10609  uzsinds  10806  iseqovex  10820  seq3val  10822  seqvalcd  10823  seqf  10826  seqovcd  10829  monoord2  10848  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seq3f1olemqsum  10875  seq3f1olemp  10877  seq3f1oleml  10878  seq3f1o  10879  nn0ltexp2  11071  bccl  11129  seq3shft  11523  caucvgre  11666  cvg1nlemcau  11669  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  cau3lem  11799  zsumdc  12070  fsum3  12073  isumz  12075  isumss2  12079  fsumsersdc  12081  fsum3ser  12083  fisum0diag2  12133  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratz  12218  mertenslem2  12222  mertensabs  12223  zproddc  12265  fprodseq  12269  prod1dc  12272  fprodsplitdc  12282  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemzz  12698  bezoutlemeu  12703  bezoutlemle  12704  dfgcd3  12706  prmind2  12817  sqrt2irr  12859  hashdvds  12918  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemr  13174  ctinfom  13179  ctinf  13181  ctiunctlemudc  13188  ssnnctlemct  13197  nninfdclemp1  13201  mplsubgfilemcl  14854  tgcn  15073  mulcncflem  15472  suplociccreex  15489  dedekindicc  15498  vtxedgfi  16284  vtxlpfi  16285  nnsf  16783  nninfsellemqall  16793  nninfomni  16797  repiecef  16812  trirec0  16828  apdiff  16832  iswomni0  16836  dceqnconst  16846  dcapnconst  16847  neap0mkv  16855  ltlenmkv  16856