Theorem ruvALT 43421

Description: Alternate proof of ruv 9566 with one fewer syntax step thanks to using elirrv 9555 instead of elirr 9558. 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 30751. (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 3459	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9555	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3067	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 267	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2898	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2772	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1570   ∈ wcel 2143  {cab 2741   ∉ wnel 3064  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-reg 9550

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nel 3065  df-v 3457

This theorem is referenced by: (None)