| 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 form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.) |
| Ref | Expression |
|---|---|
| isseti.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| isseti | ⊢ ∃𝑥 𝑥 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isseti.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | elissetv 2822 | . 2 ⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ∃𝑥 𝑥 = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 |
| This theorem is referenced by: rexcom4b 3513 ceqsal 3519 ceqsalv 3521 ceqsexOLD 3531 ceqsexv2d 3533 vtocle 3555 vtoclOLD 3559 vtoclef 3563 vtoclfOLD 3565 euind 3730 eusv2nf 5395 zfpair 5421 axprALT 5422 opabn0 5558 isarep2 6658 dfoprab2 7491 rnoprab 7538 ov3 7596 omeu 8623 cflem 10285 cflemOLD 10286 genpass 11049 supaddc 12235 supadd 12236 supmul1 12237 supmullem2 12239 supmul 12240 ruclem13 16278 joindm 18420 meetdm 18434 dmscut 27856 bnj986 34969 satfdm 35374 fmla0 35387 fmlasuc0 35389 bj-snsetex 36964 bj-restn0 37091 bj-restuni 37098 ac6s6f 38180 tfsconcatlem 43349 elintima 43666 ormklocald 46889 natlocalincr 46891 tworepnotupword 46901 funressnfv 47055 elpglem2 49231 |
| Copyright terms: Public domain | W3C validator |