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

Metamath Proof Explorer

Theorem fncnvima2

Description: Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fncnvima2 ⊢ F Fn A → F -1 B = x ∈ A | F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 elpreima ⊢ F Fn A → x ∈ F -1 B ↔ x ∈ A ∧ F ⁡ x ∈ B
2 1 eqabdv ⊢ F Fn A → F -1 B = x | x ∈ A ∧ F ⁡ x ∈ B
3 df-rab ⊢ x ∈ A | F ⁡ x ∈ B = x | x ∈ A ∧ F ⁡ x ∈ B
4 2 3 eqtr4di ⊢ F Fn A → F -1 B = x ∈ A | F ⁡ x ∈ B