Theorem ruvALT 42650

Description: Alternate proof of ruv 9561 with one fewer syntax step thanks to using elirrv 9555 instead of elirr 9556. 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 30335. (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 3454	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9555	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3033	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 264	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2864	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2739	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

Syntax hints:   = wceq 1540   ∈ wcel 2109  {cab 2708   ∉ wnel 3030  Vcvv 3450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-pr 5389  ax-reg 9551

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nel 3031  df-ral 3046  df-rex 3055  df-v 3452  df-un 3921  df-sn 4592  df-pr 4594

This theorem is referenced by: (None)