| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vex | Structured version Visualization version GIF version | ||
| Description: All setvar variables are sets (see isset 3494). Theorem 6.8 of [Quine] p. 43. A shorter proof is possible from eleq2i 2833 but it uses more axioms. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2177. (Revised by SN, 28-Aug-2023.) (Proof shortened by BJ, 4-Sep-2024.) |
| Ref | Expression |
|---|---|
| vex | ⊢ 𝑥 ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vextru 2721 | . 2 ⊢ 𝑥 ∈ {𝑥 ∣ ⊤} | |
| 2 | dfv2 3483 | . 2 ⊢ V = {𝑥 ∣ ⊤} | |
| 3 | 1, 2 | eleqtrri 2840 | 1 ⊢ 𝑥 ∈ V |
| Copyright terms: Public domain | W3C validator |