Metamath Proof Explorer


Theorem axacndlem3

Description: Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axacndlem3 y y = z x y z x y z z w w y w y z z w y w w x y = w

Proof

Step Hyp Ref Expression
1 nfae z y y = z
2 simpl y z z w y z
3 2 alimi x y z z w x y z
4 nd3 y y = z ¬ x y z
5 4 pm2.21d y y = z x y z w y w y z z w y w w x y = w
6 3 5 syl5 y y = z x y z z w w y w y z z w y w w x y = w
7 1 6 alrimi y y = z z x y z z w w y w y z z w y w w x y = w
8 7 axc4i y y = z y z x y z z w w y w y z z w y w w x y = w
9 8 19.8ad y y = z x y z x y z z w w y w y z z w y w w x y = w