Theorem abbi2i 1617

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

Syntax hints:   <-> wb 144   = wceq 992   e. wcel 994  {cab 1505

This theorem is referenced by:  abid2 1623  difeqri 2212  symdif2 2318  dfnul2 2334  dfpr2 2480  dftp2 2501  pw0 2532  iunrab 2664  0iin 2674  fv3 3844  xp2 4165  tfrlem3 4214  mapsn 4486  ixpconst 4493  ixp0x 4500  unfilem1 4694  dfom4 4778  cardnum 5039  alephiso 5042  nnzrab 6325  nn0zrab 6326  dfch2 9525  pjrni 9925

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514

Copyright terms: Public domain