Theorem ruvALT 42626

Description: Alternate proof of ruv 9673 with one fewer syntax step thanks to using elirrv 9667 instead of elirr 9668. 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 30434. (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 3492	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9667	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3055	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 264	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2880	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2749	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1537   ∈ wcel 2108  {cab 2717   ∉ wnel 3052  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-pr 5447  ax-reg 9663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nel 3053  df-ral 3068  df-rex 3077  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by: (None)