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 V [˙A / x]˙ B C A / x B A / x C

Proof

Step Hyp Ref Expression
1 sbcal [˙A / x]˙ y y B y C y [˙A / x]˙ y B y C
2 sbcimg A V [˙A / x]˙ y B y C [˙A / x]˙ y B [˙A / x]˙ y C
3 sbcel2 [˙A / x]˙ y B y A / x B
4 sbcel2 [˙A / x]˙ y C y A / x C
5 3 4 imbi12i [˙A / x]˙ y B [˙A / x]˙ y C y A / x B y A / x C
6 2 5 bitrdi A V [˙A / x]˙ y B y C y A / x B y A / x C
7 6 albidv A V y [˙A / x]˙ y B y C y y A / x B y A / x C
8 1 7 syl5bb A V [˙A / x]˙ y y B y C y y A / x B y A / x C
9 dfss2 B C y y B y C
10 9 sbcbii [˙A / x]˙ B C [˙A / x]˙ y y B y C
11 dfss2 A / x B A / x C y y A / x B y A / x C
12 8 10 11 3bitr4g A V [˙A / x]˙ B C A / x B A / x C