![]() |
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 9547 with one fewer syntax step thanks to using elirrv 9541 instead of elirr 9542. 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 29407. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ruvALT | ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3450 | . . . 4 ⊢ 𝑥 ∈ V | |
2 | elirrv 9541 | . . . . 5 ⊢ ¬ 𝑥 ∈ 𝑥 | |
3 | 2 | nelir 3048 | . . . 4 ⊢ 𝑥 ∉ 𝑥 |
4 | 1, 3 | 2th 263 | . . 3 ⊢ (𝑥 ∈ V ↔ 𝑥 ∉ 𝑥) |
5 | 4 | eqabi 2868 | . 2 ⊢ V = {𝑥 ∣ 𝑥 ∉ 𝑥} |
6 | 5 | eqcomi 2740 | 1 ⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 {cab 2708 ∉ wnel 3045 Vcvv 3446 |
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 2702 ax-sep 5261 ax-pr 5389 ax-reg 9537 |
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 2709 df-cleq 2723 df-clel 2809 df-nel 3046 df-ral 3061 df-rex 3070 df-v 3448 df-un 3918 df-sn 4592 df-pr 4594 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |