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

Theorem abeq2i 2199
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
Hypothesis
Ref Expression
abeqi.1 𝐴 = {𝑥𝜑}
Assertion
Ref Expression
abeq2i (𝑥𝐴𝜑)

Proof of Theorem abeq2i
StepHypRef Expression
1 abeqi.1 . . 3 𝐴 = {𝑥𝜑}
21eleq2i 2155 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝜑})
3 abid 2077 . 2 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
42, 3bitri 183 1 (𝑥𝐴𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1290  wcel 1439  {cab 2075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085
This theorem is referenced by:  rabid  2543  vex  2623  csbco  2943  csbnestgf  2981  ifmdc  3432  pwss  3449  snsspw  3614  iunpw  4315  ordon  4316  funcnv3  5089  tfrlem4  6092  tfrlem8  6097  tfrlem9  6098  tfrlemibxssdm  6106  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  ixpm  6501  mapsnen  6582  sbthlem1  6720  1idprl  7203  1idpru  7204  recexprlem1ssl  7246  recexprlem1ssu  7247  recexprlemss1l  7248  recexprlemss1u  7249
  Copyright terms: Public domain W3C validator