Metamath Proof Explorer


Theorem axextg

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 zzxzyx=y

Proof

Step Hyp Ref Expression
1 elequ2 w=xzwzx
2 1 bibi1d w=xzwzyzxzy
3 2 albidv w=xzzwzyzzxzy
4 equequ1 w=xw=yx=y
5 3 4 imbi12d w=xzzwzyw=yzzxzyx=y
6 ax-ext zzwzyw=y
7 5 6 chvarvv zzxzyx=y