Metamath Proof Explorer


Theorem s1prc

Description: Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022)

Ref Expression
Assertion s1prc
|- ( -. A e. _V -> <" A "> = <" (/) "> )

Proof

Step Hyp Ref Expression
1 ids1
 |-  <" A "> = <" ( _I ` A ) ">
2 fvprc
 |-  ( -. A e. _V -> ( _I ` A ) = (/) )
3 2 s1eqd
 |-  ( -. A e. _V -> <" ( _I ` A ) "> = <" (/) "> )
4 1 3 eqtrid
 |-  ( -. A e. _V -> <" A "> = <" (/) "> )