Theorem risset 2145

Description: Two ways to say "A belongs to B."

Assertion

Ref	Expression
risset	|- (A e. B <-> E.x e. B x = A)

Distinct variable groups:   x,A   x,B

Proof of Theorem risset

Step	Hyp	Ref	Expression
1		exancom 1401	. 2 |- (E.x(x e. B /\ x = A) <-> E.x(x = A /\ x e. B))
2		df-rex 2110	. 2 |- (E.x e. B x = A <-> E.x(x e. B /\ x = A))
3		df-clel 1880	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
4	1, 2, 3	3bitr4ri 201	1 |- (A e. B <-> E.x e. B x = A)

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  E.wrex 2106

This theorem is referenced by:  reuind 2450  0el 2891  iunid 3308  sucel 3738  qsid 5360  zorn 5959  negeui 6510  receui 6890  zq 7440  cnsscnp 9049  dfon2lem8 13856  prtlem9 16264  prtlem11 16268  prter2 16285

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-clel 1880  df-rex 2110

Copyright terms: Public domain