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

Metamath Proof Explorer

Theorem f1imaeq

Description: Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Assertion f1imaeq ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 f1imass ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊆ 𝐷 ) )
2 f1imass ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐷 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ↔ 𝐷 ⊆ 𝐶 ) )
3 2 ancom2s ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ↔ 𝐷 ⊆ 𝐶 ) )
4 1 3 anbi12d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐶 ) ) )
5 eqss ⊢ ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ) )
6 eqss ⊢ ( 𝐶 = 𝐷 ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐶 ) )
7 4 5 6 3bitr4g ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ 𝐶 = 𝐷 ) )