Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > isseti | GIF version |
Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
isseti.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
isseti | ⊢ ∃𝑥 𝑥 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isseti.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | isset 2692 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ ∃𝑥 𝑥 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1331 ∃wex 1468 ∈ wcel 1480 Vcvv 2686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-v 2688 |
This theorem is referenced by: rexcom4b 2711 ceqsex 2724 vtoclf 2739 vtocl2 2741 vtocl3 2742 vtoclef 2759 eqvinc 2808 euind 2871 opabm 4202 eusv2nf 4377 dtruex 4474 limom 4527 isarep2 5210 dfoprab2 5818 rnoprab 5854 dmaddpq 7187 dmmulpq 7188 bj-inf2vnlem1 13168 |
Copyright terms: Public domain | W3C validator |