Theorem ruvALT 43823

Description: Alternate proof of ruv 9615 with one fewer syntax step thanks to using elirrv 9604 instead of elirr 9607. 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 31016. (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 3458	. . . 4 ⊢ 𝑥 ∈ V
2		elirrv 9604	. . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥
3	2	nelir 3068	. . . 4 ⊢ 𝑥 ∉ 𝑥
4	1, 3	2th 267	. . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥)
5	4	eqabi 2899	. 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥}
6	5	eqcomi 2772	1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  {cab 2741   ∉ wnel 3065  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-reg 9599

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-nel 3066  df-v 3456

This theorem is used by: (None)