Metamath Proof Explorer


Theorem fniniseg2

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

Ref Expression
Assertion fniniseg2 F Fn A F -1 B = x A | F x = B

Proof

Step Hyp Ref Expression
1 fncnvima2 F Fn A F -1 B = x A | F x B
2 fvex F x V
3 2 elsn F x B F x = B
4 3 rabbii x A | F x B = x A | F x = B
5 1 4 eqtrdi F Fn A F -1 B = x A | F x = B