Theorem ruvALT 39831

Description: Alternate proof of ruv 9196 with one fewer syntax step thanks to using elirrv 9190 instead of elirr 9191. 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 28437. (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 3402	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9190	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3039	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 267	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	abbi2i 2869	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2745	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1543   ∈ wcel 2112  {cab 2714   ∉ wnel 3036  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-reg 9186

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-nel 3037  df-ral 3056  df-rex 3057  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-sn 4528  df-pr 4530

This theorem is referenced by: (None)