Theorem cbvralv 2577

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

Syntax hints:   → wi 4   ↔ wb 103  ∀wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353

This theorem is referenced by:  cbvral2v  2585  cbvral3v  2587  reu7  2787  reusv3i  4209  cnvpom  4880  f1mpt  5431  grprinvlem  5715  grprinvd  5716  tfrlem1  5946  tfrlemiubacc  5967  tfrlemi1  5969  rdgon  5996  nneneq  6343  supubti  6412  suplubti  6413  cauappcvgprlemladdrl  6847  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgsrlembound  6970  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  peano5nnnn  7058  axcaucvglemres  7065  suprleubex  8032  nnsub  8077  supinfneg  8683  infsupneg  8684  ublbneg  8698  uzsinds  9428  iseqovex  9439  iseqval  9440  monoord2  9456  bccl  9694  caucvgre  9867  cvg1nlemcau  9870  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  cau3lem  10000  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemeu  10396  bezoutlemle  10397  dfgcd3  10399  prmind2  10502  sqrt2irr  10541