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

Theorem abbi2i 2252
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbiri.1  |-  ( x  e.  A  <->  ph )
Assertion
Ref Expression
abbi2i  |-  A  =  { x  |  ph }
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2246 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
2 abbiri.1 . 2  |-  ( x  e.  A  <->  ph )
31, 2mpgbir 1429 1  |-  A  =  { x  |  ph }
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1331    e. wcel 1480   {cab 2123
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-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133
This theorem is referenced by:  abid2  2258  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  symdifxor  3337  dfnul2  3360  dfpr2  3541  dftp2  3567  0iin  3866  pwpwab  3895  epse  4259  fv3  5437  fo1st  6048  fo2nd  6049  xp2  6064  tfrlem3  6201  tfr1onlem3  6228  mapsn  6577  ixpconstg  6594  ixp0x  6613  nnzrab  9071  nn0zrab  9072
  Copyright terms: Public domain W3C validator