Theorem abbi2i 1577

Description: Equality of a class variable and a class abstraction (inference rule).

Hypothesis

Ref	Expression
abbiri.1	|- (x e. A <-> ph)

Assertion

Ref	Expression
abbi2i	|- A = {x | ph}

Distinct variable group:   x,A

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abeq2 1571	. 2 |- (A = {x | ph} <-> A.x(x e. A <-> ph))
2		abbiri.1	. 2 |- (x e. A <-> ph)
3	1, 2	mpgbir 990	1 |- A = {x | ph}

Syntax hints:   <-> wb 146   = wceq 958   e. wcel 960  {cab 1466

This theorem is referenced by:  abid2 1583  difeqri 2163  symdif2 2269  dfnul2 2285  dfpr2 2426  dftp2 2444  pw0 2472  iunrab 2600  0iin 2610  fv3 3739  tfrlem3 3919  xp2 4111  mapsn 4351  ixpconst 4358  ixp0x 4365  unfilem1 4560  dfom4 4641  cardnum 4900  alephiso 4903  nnzrab 6159  nn0zrab 6160  dfch2 9244  pjrn 9642

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475

Copyright terms: Public domain