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 syl5eq 
 |-  ( -. A e. _V -> <" A "> = <" (/) "> )