Metamath Proof Explorer

Theorem csb0

Description: The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018)

Ref Expression
Assertion csb0 
|- [_ A / x ]_ (/) = (/)

Proof

Step Hyp Ref Expression
1 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ (/) = (/) )
2 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ (/) = (/) )
3 1 2 pm2.61i 
 |-  [_ A / x ]_ (/) = (/)