Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof shortened by Wolf Lammen, 10-May-2023) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfabd2.1 | |
|
nfabd2.2 | |
||
Assertion | nfabd2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfabd2.1 | |
|
2 | nfabd2.2 | |
|
3 | nfnae | |
|
4 | 1 3 | nfan | |
5 | 4 2 | nfabd | |
6 | 5 | ex | |
7 | nfab1 | |
|
8 | eqidd | |
|
9 | 8 | drnfc1 | |
10 | 7 9 | mpbiri | |
11 | 6 10 | pm2.61d2 | |