This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbsng

Description: Distribute proper substitution through the singleton of a class. csbsng is derived from the virtual deduction proof csbsngVD . (Contributed by Alan Sare, 10-Nov-2012)

Ref Expression
Assertion csbsng 
|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )

Proof

Step Hyp Ref Expression
1 csbab 
 |-  [_ A / x ]_ { y | y = B } = { y | [. A / x ]. y = B }
2 sbceq2g 
 |-  ( A e. V -> ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) )
3 2 abbidv 
 |-  ( A e. V -> { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } )
4 1 3 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } )
5 df-sn 
 |-  { B } = { y | y = B }
6 5 csbeq2i 
 |-  [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B }
7 df-sn 
 |-  { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B }
8 4 6 7 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )