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

Proof

Step Hyp Ref Expression
1 eqfnfv2 ⊢FFnA∧GFnB→F=G↔A=B∧∀x∈AF⁡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∈AF⁡x=G⁡x↔B⊆A∧A⊆B∧∀x∈AF⁡x=G⁡x
5 anass ⊢B⊆A∧A⊆B∧∀x∈AF⁡x=G⁡x↔B⊆A∧A⊆B∧∀x∈AF⁡x=G⁡x
6 dfss3 ⊢A⊆B↔∀x∈Ax∈B
7 6 anbi1i ⊢A⊆B∧∀x∈AF⁡x=G⁡x↔∀x∈Ax∈B∧∀x∈AF⁡x=G⁡x
8 r19.26 ⊢∀x∈Ax∈B∧F⁡x=G⁡x↔∀x∈Ax∈B∧∀x∈AF⁡x=G⁡x
9 7 8 bitr4i ⊢A⊆B∧∀x∈AF⁡x=G⁡x↔∀x∈Ax∈B∧F⁡x=G⁡x
10 9 anbi2i ⊢B⊆A∧A⊆B∧∀x∈AF⁡x=G⁡x↔B⊆A∧∀x∈Ax∈B∧F⁡x=G⁡x
11 4 5 10 3bitri ⊢A=B∧∀x∈AF⁡x=G⁡x↔B⊆A∧∀x∈Ax∈B∧F⁡x=G⁡x
12 1 11 bitrdi ⊢FFnA∧GFnB→F=G↔B⊆A∧∀x∈Ax∈B∧F⁡x=G⁡x