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 ⊢ F Fn A ∧ G Fn B → F = G ↔ B ⊆ A ∧ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x

Proof

Step Hyp Ref Expression
1 eqfnfv2 ⊢ F Fn A ∧ G Fn B → F = G ↔ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
2 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
3 2 biancomi ⊢ A = B ↔ B ⊆ A ∧ A ⊆ B
4 3 anbi1i ⊢ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ B ⊆ A ∧ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
5 anass ⊢ B ⊆ A ∧ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ B ⊆ A ∧ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
6 dfss3 ⊢ A ⊆ B ↔ ∀ x ∈ A x ∈ B
7 6 anbi1i ⊢ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ ∀ x ∈ A x ∈ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
8 r19.26 ⊢ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x ↔ ∀ x ∈ A x ∈ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
9 7 8 bitr4i ⊢ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x
10 9 anbi2i ⊢ B ⊆ A ∧ A ⊆ B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ B ⊆ A ∧ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x
11 4 5 10 3bitri ⊢ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x ↔ B ⊆ A ∧ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x
12 1 11 bitrdi ⊢ F Fn A ∧ G Fn B → F = G ↔ B ⊆ A ∧ ∀ x ∈ A x ∈ B ∧ F ⁡ x = G ⁡ x