Description: A generalization of the axiom of extensionality in which x and y need not be distinct. (Contributed by NM, 15-Sep-1993) (Proof shortened by Andrew Salmon, 12-Aug-2011) Remove dependencies on ax-10 , ax-12 , ax-13 . (Revised by BJ, 12-Jul-2019) (Revised by Wolf Lammen, 9-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | axextg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 | |
|
2 | 1 | bibi1d | |
3 | 2 | albidv | |
4 | equequ1 | |
|
5 | 3 4 | imbi12d | |
6 | ax-ext | |
|
7 | 5 6 | chvarvv | |