Theorem ruvALT 42642

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {cab 2712   ∉ wnel 3035  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-pr 5412  ax-reg 9614

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nel 3036  df-ral 3051  df-rex 3060  df-v 3465  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by: (None)