![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isseti | Structured version Visualization version GIF version |
Description: A way to say "𝐴 is a set" (inference rule). (Contributed by NM, 24-Jun-1993.) |
Ref | Expression |
---|---|
isseti.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
isseti | ⊢ ∃𝑥 𝑥 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isseti.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | isset 3238 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ ∃𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∃wex 1744 ∈ wcel 2030 Vcvv 3231 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-12 2087 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-tru 1526 df-ex 1745 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-v 3233 |
This theorem is referenced by: rexcom4b 3258 ceqsex 3272 vtoclf 3289 vtocl 3290 vtocl2 3292 vtocl3 3293 vtoclef 3312 euind 3426 eusv2nf 4894 zfpair 4934 axpr 4935 opabn0 5035 isarep2 6016 dfoprab2 6743 rnoprab 6785 ov3 6839 omeu 7710 cflem 9106 genpass 9869 supaddc 11028 supadd 11029 supmul1 11030 supmullem2 11032 supmul 11033 ruclem13 15015 joindm 17050 meetdm 17064 bnj986 31150 bj-snsetex 33076 bj-restn0 33168 bj-restuni 33175 ac6s6f 34111 elintima 38262 funressnfv 41529 elpglem2 42783 |
Copyright terms: Public domain | W3C validator |