Metamath Proof Explorer


Theorem fviss

Description: The value of the identity function is a subset of the argument. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Assertion fviss IAA

Proof

Step Hyp Ref Expression
1 id xIAxIA
2 elfvex xIAAV
3 fvi AVIA=A
4 2 3 syl xIAIA=A
5 1 4 eleqtrd xIAxA
6 5 ssriv IAA