Theorem risset 2661

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 2620	. 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 2615

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 2620

This theorem is referenced by:  reueq  3033  reuind  3039  0el  3566  iunid  4021  snelpw1  4146  unipw1  4325  addcid1  4405  nncaddccl  4419  vfinspsslem1  4550  vfinspclt  4552  nulnnn  4556  dfproj12  4576  dfproj22  4577  proj1op  4600  proj2op  4601  phidisjnn  4615  phialllem1  4616  dfdm4  5507  dfrn5  5508  oqelins4  5794  otsnelsi3  5805  addcfnex  5824  funsex  5828  qsid  5990  mapexi  6003  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  ovcelem1  6171  ce0nn  6180  finnc  6243  nncdiv3lem1  6275  nchoicelem11  6299  nchoicelem12  6300  nchoicelem17  6305  nchoicelem18  6306