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

Metamath Proof Explorer

Theorem csbidm

Description: Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion csbidm 
|- [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B

Proof

Step Hyp Ref Expression
1 csbnest1g 
 |-  ( A e. _V -> [_ A / x ]_ [_ A / x ]_ B = [_ [_ A / x ]_ A / x ]_ B )
2 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ A = A )
3 2 csbeq1d 
 |-  ( A e. _V -> [_ [_ A / x ]_ A / x ]_ B = [_ A / x ]_ B )
4 1 3 eqtrd 
 |-  ( A e. _V -> [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B )
5 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ [_ A / x ]_ B = (/) )
6 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
7 5 6 eqtr4d 
 |-  ( -. A e. _V -> [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B )
8 4 7 pm2.61i 
 |-  [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B