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	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvfo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		cbvfo.1	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		fofn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
3	1	bicomd	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
4	3	eqcoms	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝜓 ↔ 𝜑 ) )
5	4	ralrn	⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑦 ∈ ran 𝐹 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
6	2 5	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑦 ∈ ran 𝐹 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
7		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
8	7	raleqdv	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑦 ∈ ran 𝐹 𝜓 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )
9	6 8	bitr3d	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )