Theorem ruvALT 43251

Description: Alternate proof of ruv 9556 with one fewer syntax step thanks to using elirrv 9545 instead of elirr 9548. 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 30602. (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 3458	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9545	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3064	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 266	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2897	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2771	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1560   ∈ wcel 2142  {cab 2740   ∉ wnel 3061  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-reg 9540

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nel 3062  df-v 3456

This theorem is referenced by: (None)