Theorem ruvALT 43680

Description: Alternate proof of ruv 9602 with one fewer syntax step thanks to using elirrv 9591 instead of elirr 9594. 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 31001. (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 3455	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9591	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3065	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 267	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2896	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2770	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2739   ∉ wnel 3062  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-reg 9586

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nel 3063  df-v 3453

This theorem is used by: (None)