Theorem cbvralv 2657

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422

This theorem is referenced by:  cbvralvw  2661  cbvral2v  2668  cbvral3v  2670  reu7  2883  reusv3i  4388  omsinds  4543  cnvpom  5089  f1mpt  5680  grprinvlem  5973  grprinvd  5974  tfrlem1  6213  tfrlemiubacc  6235  tfrlemi1  6237  tfr1onlemubacc  6251  tfr1onlemaccex  6253  tfrcllembxssdm  6261  tfrcllemubacc  6264  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  rdgon  6291  frecfcllem  6309  frecsuclem  6311  nneneq  6759  fimax2gtrilemstep  6802  supubti  6894  suplubti  6895  finomni  7020  acfun  7080  ccfunen  7096  cc2  7099  cauappcvgprlemladdrl  7489  caucvgprlemcl  7508  caucvgprlemladdrl  7510  caucvgsrlembound  7626  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  suplocsrlem  7640  peano5nnnn  7724  axcaucvglemres  7731  axpre-suploc  7734  suprleubex  8736  nnsub  8783  supinfneg  9417  infsupneg  9418  ublbneg  9432  exbtwnzlemex  10058  uzsinds  10246  iseqovex  10260  seq3val  10262  seqvalcd  10263  seqf  10265  seqovcd  10267  monoord2  10281  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  seq3f1olemqsum  10304  seq3f1olemp  10306  seq3f1oleml  10307  seq3f1o  10308  bccl  10545  seq3shft  10642  caucvgre  10785  cvg1nlemcau  10788  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  cau3lem  10918  zsumdc  11185  fsum3  11188  isumz  11190  isumss2  11194  fsumsersdc  11196  fsum3ser  11198  fisum0diag2  11248  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratz  11333  mertenslem2  11337  mertensabs  11338  zproddc  11380  fprodseq  11384  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemeu  11731  bezoutlemle  11732  dfgcd3  11734  prmind2  11837  sqrt2irr  11876  hashdvds  11933  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemr  11972  ctinfom  11977  ctinf  11979  ctiunctlemudc  11986  tgcn  12416  mulcncflem  12798  suplociccreex  12810  dedekindicc  12819  nnsf  13374  nninfsellemqall  13386  nninfomni  13390  trirec0  13412  apdiff  13416  dceqnconst  13423