![]() |
Mathbox for Steven Nguyen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ruvALT | Structured version Visualization version GIF version |
Description: Alternate proof of ruv 9538 with one fewer syntax step thanks to using elirrv 9532 instead of elirr 9533. 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 29344. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ruvALT | ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3449 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | elirrv 9532 | . . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥 | |
3 | 2 | nelir 3052 | . . . 4 ⊢ 𝑥 ∉ 𝑥 |
4 | 1, 3 | 2th 263 | . . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥) |
5 | 4 | abbi2i 2873 | . 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥} |
6 | 5 | eqcomi 2745 | 1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 {cab 2713 ∉ wnel 3049 Vcvv 3445 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-pr 5384 ax-reg 9528 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-nel 3050 df-ral 3065 df-rex 3074 df-v 3447 df-un 3915 df-sn 4587 df-pr 4589 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |