Description: A version of rabexg using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rabexgf.1 | ||
Assertion | rabexgf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabexgf.1 | ||
2 | df-rab | ||
3 | simpl | ||
4 | 3 | ss2abi | |
5 | 1 | abid2f | |
6 | 4 5 | sseqtri | |
7 | 2 6 | eqsstri | |
8 | ssexg | ||
9 | 7 8 | mpan |