![]() |
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 2813 | . 2 ⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∃𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∃wex 1781 ∈ wcel 2106 Vcvv 3473 |
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 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-clel 2809 |
This theorem is referenced by: rexcom4b 3502 ceqsal 3507 ceqsalv 3509 ceqsexOLD 3521 ceqsexvOLD 3523 vtoclef 3543 vtoclfOLD 3545 vtocl 3546 euind 3716 eusv2nf 5386 zfpair 5412 axprALT 5413 opabn0 5546 isarep2 6628 dfoprab2 7451 rnoprab 7496 ov3 7553 omeu 8568 cflem 10223 genpass 10986 supaddc 12163 supadd 12164 supmul1 12165 supmullem2 12167 supmul 12168 ruclem13 16167 joindm 18310 meetdm 18324 dmscut 27238 bnj986 33795 satfdm 34189 fmla0 34202 fmlasuc0 34204 bj-snsetex 35646 bj-restn0 35773 bj-restuni 35780 ac6s6f 36844 tfsconcatlem 41855 elintima 42173 natlocalincr 45361 tworepnotupword 45371 funressnfv 45523 elpglem2 47403 |
Copyright terms: Public domain | W3C validator |