Description: Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pwsdiagel.y | ||
pwsdiagel.b | |||
pwsdiagel.c | |||
Assertion | pwsdiagel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwsdiagel.y | ||
2 | pwsdiagel.b | ||
3 | pwsdiagel.c | ||
4 | fconst6g | ||
5 | 4 | adantl | |
6 | 1 2 3 | pwselbasb | |
7 | 6 | adantr | |
8 | 5 7 | mpbird |