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 3180 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ ∃𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 |
This theorem is referenced by: rexcom4b 3200 ceqsex 3214 vtoclf 3231 vtocl 3232 vtocl2 3234 vtocl3 3235 vtoclef 3254 eqvinc 3300 euind 3360 eusv2nf 4790 zfpair 4831 axpr 4832 opabn0 4931 isarep2 5892 dfoprab2 6599 rnoprab 6641 ov3 6695 omeu 7552 cflem 8951 genpass 9710 supaddc 10867 supadd 10868 supmul1 10869 supmullem2 10871 supmul 10872 ruclem13 14810 joindm 16826 meetdm 16840 bnj986 30278 bj-snsetex 32144 bj-restn0 32224 bj-restuni 32231 ac6s6f 33151 elintima 36964 funressnfv 39857 elpglem2 42254 |
Copyright terms: Public domain | W3C validator |