Theorem ruvALT 43293

Description: Alternate proof of ruv 9570 with one fewer syntax step thanks to using elirrv 9559 instead of elirr 9562. 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 30692. (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 3467	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9559	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3073	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 267	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2904	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2778	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1567   ∈ wcel 2149  {cab 2747   ∉ wnel 3070  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-reg 9554

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nel 3071  df-v 3465

This theorem is referenced by: (None)