Theorem risset 2662

Description: Two ways to say "A belongs to B." (Contributed by NM, 22-Nov-1994.)

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 1586	. 2 |- (E.x(x e. B /\ x = A) <-> E.x(x = A /\ x e. B))
2		df-rex 2621	. 2 |- (E.x e. B x = A <-> E.x(x e. B /\ x = A))
3		df-clel 2349	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
4	1, 2, 3	3bitr4ri 269	1 |- (A e. B <-> E.x e. B x = A)

Syntax hints:   <-> wb 176   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-clel 2349  df-rex 2621

This theorem is referenced by:  reueq  3034  reuind  3040  0el  3567  iunid  4022  snelpw1  4147  unipw1  4326  addcid1  4406  nncaddccl  4420  vfinspsslem1  4551  vfinspclt  4553  nulnnn  4557  dfproj12  4577  dfproj22  4578  proj1op  4601  proj2op  4602  phidisjnn  4616  phialllem1  4617  dfdm4  5508  dfrn5  5509  oqelins4  5795  otsnelsi3  5806  addcfnex  5825  funsex  5829  qsid  5991  mapexi  6004  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  ovcelem1  6172  ce0nn  6181  finnc  6244  nncdiv3lem1  6276  nchoicelem11  6300  nchoicelem12  6301  nchoicelem17  6306  nchoicelem18  6307