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 syl5bb
 |-  ( 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 ) )