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

Theorem abbi2i 2209
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbiri.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
abbi2i 𝐴 = {𝑥𝜑}
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2203 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
2 abbiri.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1394 1 𝐴 = {𝑥𝜑}
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1296  wcel 1445  {cab 2081
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 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091
This theorem is referenced by:  abid2  2215  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  symdifxor  3281  dfnul2  3304  dfpr2  3485  dftp2  3511  0iin  3810  pwpwab  3838  epse  4193  fv3  5363  fo1st  5966  fo2nd  5967  xp2  5981  tfrlem3  6114  tfr1onlem3  6141  mapsn  6487  ixpconstg  6504  ixp0x  6523  nnzrab  8872  nn0zrab  8873
  Copyright terms: Public domain W3C validator