Theorem ruvALT 43102

Description: Alternate proof of ruv 9522 with one fewer syntax step thanks to using elirrv 9512 instead of elirr 9514. 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 30470. (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 3433	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9512	. . . . 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 1542   ∈ wcel 2114  {cab 2714   ∉ wnel 3036  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-reg 9507

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nel 3037  df-v 3431

This theorem is referenced by: (None)