Theorem ruvALT 43119

Description: Alternate proof of ruv 9516 with one fewer syntax step thanks to using elirrv 9506 instead of elirr 9508. 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 30488. (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 3434	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9506	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3040	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 264	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2872	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2746	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2715   ∉ wnel 3037  Vcvv 3430

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 2709  ax-sep 5232  ax-pr 5371  ax-reg 9501

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 2716  df-cleq 2729  df-clel 2812  df-nel 3038  df-v 3432

This theorem is referenced by: (None)