Theorem eqfnfv3

Description: Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	eqfnfv3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
2		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
3	2	biancomi	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) )
4	3	anbi1i	⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
5		anass	⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
6		dfss3	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
7	6	anbi1i	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
8		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
9	7 8	bitr4i	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
10	9	anbi2i	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
11	4 5 10	3bitri	⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
12	1 11	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )