Metamath Proof Explorer

Theorem sbcssg

Description: Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012) (Proof shortened by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion sbcssg 
|- ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 sbcal 
 |-  ( [. A / x ]. A. y ( y e. B -> y e. C ) <-> A. y [. A / x ]. ( y e. B -> y e. C ) )
2 sbcimg 
 |-  ( A e. V -> ( [. A / x ]. ( y e. B -> y e. C ) <-> ( [. A / x ]. y e. B -> [. A / x ]. y e. C ) ) )
3 sbcel2 
 |-  ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B )
4 sbcel2 
 |-  ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C )
5 3 4 imbi12i 
 |-  ( ( [. A / x ]. y e. B -> [. A / x ]. y e. C ) <-> ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) )
6 2 5 bitrdi 
 |-  ( A e. V -> ( [. A / x ]. ( y e. B -> y e. C ) <-> ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) )
7 6 albidv 
 |-  ( A e. V -> ( A. y [. A / x ]. ( y e. B -> y e. C ) <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) )
8 1 7 bitrid 
 |-  ( A e. V -> ( [. A / x ]. A. y ( y e. B -> y e. C ) <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) )
9 dfss2 
 |-  ( B C_ C <-> A. y ( y e. B -> y e. C ) )
10 9 sbcbii 
 |-  ( [. A / x ]. B C_ C <-> [. A / x ]. A. y ( y e. B -> y e. C ) )
11 dfss2 
 |-  ( [_ A / x ]_ B C_ [_ A / x ]_ C <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) )
12 8 10 11 3bitr4g 
 |-  ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) )