Theorem ruvALT 42922

Description: Alternate proof of ruv 9510 with one fewer syntax step thanks to using elirrv 9502 instead of elirr 9504. However, it does not change the compressed proof size or the number of symbols in the generated display, so it is not considered a shortening according to conventions 30475. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
ruvALT	⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Proof of Theorem ruvALT

Step	Hyp	Ref	Expression
1		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9502	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3039	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 264	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2871	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2745	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2714   ∉ wnel 3036  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pr 5377  ax-reg 9497

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nel 3037  df-v 3442

This theorem is referenced by: (None)