HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef 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))
41, 2, 33bitr4ri 201 1 |- (A e. B <-> E.x e. B x = A)
Colors of variables: wff set class
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