Theorem ruvALT 42662

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {cab 2707   ∉ wnel 3029  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-pr 5374  ax-reg 9503

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nel 3030  df-v 3440

This theorem is referenced by: (None)