Theorem abbi2i 1571

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

Hypothesis

Ref	Expression
abbiri.1	⊢ (x ∈ A ↔ φ)

Assertion

Ref	Expression
abbi2i	⊢ A = {x∣φ}

Distinct variable group:   x,A

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abeq2 1565	. 2 ⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ φ))
2		abbiri.1	. 2 ⊢ (x ∈ A ↔ φ)
3	1, 2	mpgbir 986	1 ⊢ A = {x∣φ}

Syntax hints:   ↔ wb 146   = wceq 954   ∈ wcel 956  {cab 1461

This theorem is referenced by:  abid2 1577  difeqri 2156  symdif2 2262  dfnul2 2278  dfpr2 2418  dftp2 2436  pw0 2464  iunrab 2591  0iin 2601  fv3 3724  tfrlem3 3904  xp2 4095  mapsn 4335  ixpconst 4342  ixp0x 4349  unfilem1 4530  dfom4 4612  cardnum 4869  alephiso 4872  nnzrab 6112  nn0zrab 6113  dfch2 9187  pjrn 9587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470

Copyright terms: Public domain