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

Theorem abbi2i 2130
Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbiri.1 (x Aφ)
Assertion
Ref Expression
abbi2i A = {xφ}
Distinct variable group:   x,A
Allowed substitution hint:   φ(x)

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2124 . 2 (A = {xφ} ↔ x(x Aφ))
2 abbiri.1 . 2 (x Aφ)
31, 2mpgbir 1318 1 A = {xφ}
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1226   wcel 1370  {cab 2004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014
This theorem is referenced by:  abid2  2136  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  symdifxor  3176  dfnul2  3199  dfpr2  3362  dftp2  3389  0iin  3685  epse  4043  fv3  5118  fo1st  5703  fo2nd  5704  xp2  5718  tfrlem3  5844
  Copyright terms: Public domain W3C validator