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 I A A


Step Hyp Ref Expression
1 id x I A x I A
2 elfvex x I A A V
3 fvi A V I A = A
4 2 3 syl x I A I A = A
5 1 4 eleqtrd x I A x A
6 5 ssriv I A A