This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvfo

Description: Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis cbvfo.1 ⊢ F ⁡ x = y → φ ↔ ψ
Assertion cbvfo ⊢ F : A ⟶ onto B → ∀ x ∈ A φ ↔ ∀ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 cbvfo.1 ⊢ F ⁡ x = y → φ ↔ ψ
2 fofn ⊢ F : A ⟶ onto B → F Fn A
3 1 bicomd ⊢ F ⁡ x = y → ψ ↔ φ
4 3 eqcoms ⊢ y = F ⁡ x → ψ ↔ φ
5 4 ralrn ⊢ F Fn A → ∀ y ∈ ran ⁡ F ψ ↔ ∀ x ∈ A φ
6 2 5 syl ⊢ F : A ⟶ onto B → ∀ y ∈ ran ⁡ F ψ ↔ ∀ x ∈ A φ
7 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
8 7 raleqdv ⊢ F : A ⟶ onto B → ∀ y ∈ ran ⁡ F ψ ↔ ∀ y ∈ B ψ
9 6 8 bitr3d ⊢ F : A ⟶ onto B → ∀ x ∈ A φ ↔ ∀ y ∈ B ψ