Metamath Proof Explorer


Theorem sbthlem1

Description: Lemma for sbth . (Contributed by NM, 22-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 A V
sbthlem.2 D = x | x A g B f x A x
Assertion sbthlem1 D A g B f D

Proof

Step Hyp Ref Expression
1 sbthlem.1 A V
2 sbthlem.2 D = x | x A g B f x A x
3 unissb D A g B f D x D x A g B f D
4 2 abeq2i x D x A g B f x A x
5 difss2 g B f x A x g B f x A
6 ssconb x A g B f x A x A g B f x g B f x A x
7 6 exbiri x A g B f x A g B f x A x x A g B f x
8 5 7 syl5 x A g B f x A x g B f x A x x A g B f x
9 8 pm2.43d x A g B f x A x x A g B f x
10 9 imp x A g B f x A x x A g B f x
11 4 10 sylbi x D x A g B f x
12 elssuni x D x D
13 imass2 x D f x f D
14 sscon f x f D B f D B f x
15 12 13 14 3syl x D B f D B f x
16 imass2 B f D B f x g B f D g B f x
17 sscon g B f D g B f x A g B f x A g B f D
18 15 16 17 3syl x D A g B f x A g B f D
19 11 18 sstrd x D x A g B f D
20 3 19 mprgbir D A g B f D