Theorem ruvALT 43027

Description: Alternate proof of ruv 9522 with one fewer syntax step thanks to using elirrv 9514 instead of elirr 9516. 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 30487. (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 3446	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9514	. . . . 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 3442

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 5243  ax-pr 5379  ax-reg 9509

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 3444

This theorem is referenced by: (None)