Theorem cbvralv 1807

Description: Change the bound variable of a restricted universal quantifier using implicit substitution.

Hypothesis

Ref	Expression
cbvralv.1	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
cbvralv	⊢ (∀x ∈ A φ ↔ ∀y ∈ A ψ)

Distinct variable groups:   φ,y   ψ,x   x,y,A

Proof of Theorem cbvralv

Step	Hyp	Ref	Expression
1		ax-17 975	. 2 ⊢ (φ → ∀yφ)
2		ax-17 975	. 2 ⊢ (ψ → ∀xψ)
3		cbvralv.1	. 2 ⊢ (x = y → (φ ↔ ψ))
4	1, 2, 3	cbvral 1805	1 ⊢ (∀x ∈ A φ ↔ ∀y ∈ A ψ)

Syntax hints:   → wi 3   ↔ wb 146   = wceq 960  ∀wral 1652

This theorem is referenced by:  cbvral2v 1810  cbvral3v 1811  reu7 1942  dfwe2 2951  tfinds 3177  cnvpo 3538  tfrlem1 3927  rdglem1 3953  tz7.48lem 3971  nneneq 4532  supmo 4591  supmaxlem 4603  aceq1 4746  aceq2 4748  aceq5 4757  kmlem12 4793  kmlem14 4795  zorn2lem7 4811  zorn2 4813  nnleltp1 5968  xrub 6112  supxrre 6115  uzwo3lem2 6252  uzwo3 6253  uzwo 6423  uzwoOLD 6424  fsequb 6491  sqr2irrlem3 6758  cau3iri 6947  cvg2i 6954  faclbnd4lem4 6983  bccl2 7003  caucvg3 7200  cvgcmp3cetlem1 7220  cvgcmp3cetlem2 7221  isum1pi 7238  isummulc1iALT 7245  negfcncfi 7301  acdc3 7520  acdc2 7523  acdc5 7526  acdc 7528  elcls3 7737  grpideu 8079  ubthlem1 8554  spwmo 8681  sincolem 8689  pilem2 8696  grothinf 8805  hlimcauii 9130  adjsym 9783  lnopunilem1 9959  elunop2 9962  lnophm 9968  lnopconi 9987  cnlnadjlem5 10028  mdbr3 10249  mdbr4 10250  dmdbr3 10257  dmdbr4 10258  mddmd2 10261  cayleylem2 10435

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-cleq 1475  df-clel 1478  df-ral 1656

Copyright terms: Public domain