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

Metamath Proof Explorer

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 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) )