Theorem ruvALT 43119

Description: Alternate proof of ruv 9513 with one fewer syntax step thanks to using elirrv 9502 instead of elirr 9505. 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 30488. (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 3435	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9502	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3041	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 265	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2874	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2748	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1547   ∈ wcel 2119  {cab 2717   ∉ wnel 3038  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-reg 9497

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nel 3039  df-v 3433

This theorem is referenced by: (None)