Theorem cbvralv 1333

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 group(s):   φ,y   ψ,x   x,y,A

Proof of Theorem cbvralv

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

Syntax hints:   → wi 2   ↔ wb 127   = weq 797  ∀wral 1201

This theorem is referenced by:  cbvral2v 1336  supmo 2156  dfwe2 2187  tfinds 2401  tfrlem1 2949  rdglem1 2975  tz7.48lem 2993  nneneq 3408  fiint 3445  aceq1 3552  aceq2 3554  aceq5 3563  kmlem11 3590  kmlem14 3593  zornlem7 3609  zorn 3611  nnleltp1t 4448  uzwo3lem2 4615  uzwo3 4616  sqr2irrlem3 4779  hlimcaui 5141  mdbr3 5729  mdbr4 5730

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099  df-ral 1205

metamath.org