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/xA/xB=A/xB

Proof

Step Hyp Ref Expression
1 csbnest1g AVA/xA/xB=A/xA/xB
2 csbconstg AVA/xA=A
3 2 csbeq1d AVA/xA/xB=A/xB
4 1 3 eqtrd AVA/xA/xB=A/xB
5 csbprc ¬AVA/xA/xB=
6 csbprc ¬AVA/xB=
7 5 6 eqtr4d ¬AVA/xA/xB=A/xB
8 4 7 pm2.61i A/xA/xB=A/xB