Theorem abbi2i 1550

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 1544	. 2 |- (A = {x | ph} <-> A.x(x e. A <-> ph))
2		abbiri.1	. 2 |- (x e. A <-> ph)
3	1, 2	mpgbir 964	1 |- A = {x | ph}

Syntax hints:   <-> wb 146   = wceq 1099   e. wcel 1105  {cab 1440

This theorem is referenced by:  abid2 1556  difeqri 2131  symdif2 2237  dfnul2 2253  dfpr2 2393  dftp2 2411  pw0 2438  iunrab 2564  0iin 2574  fv3 3672  tfrlem3 3852  xp2 4043  mapsn 4283  ixpconst 4290  ixp0x 4297  unfilem1 4476  dfom4 4556  cardnum 4812  alephiso 4815  nnzrab 6055  nn0zrab 6056  dfch2 9378  pjrn 9778

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449

Copyright terms: Public domain