Theorem ruvALT 42854

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2712   ∉ wnel 3034  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pr 5375  ax-reg 9495

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nel 3035  df-v 3440

This theorem is referenced by: (None)