ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isseti GIF version

Theorem isseti 2738
Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
isseti.1 𝐴 ∈ V
Assertion
Ref Expression
isseti 𝑥 𝑥 = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2 𝐴 ∈ V
2 isset 2736 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 144 1 𝑥 𝑥 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1348  wex 1485  wcel 2141  Vcvv 2730
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732
This theorem is referenced by:  rexcom4b  2755  ceqsex  2768  vtoclf  2783  vtocl2  2785  vtocl3  2786  vtoclef  2803  eqvinc  2853  euind  2917  opabm  4263  eusv2nf  4439  dtruex  4541  limom  4596  isarep2  5283  dfoprab2  5897  rnoprab  5933  dmaddpq  7328  dmmulpq  7329  bj-inf2vnlem1  13927
  Copyright terms: Public domain W3C validator