Theorem elex 1810

Description: An element of a class exists.

Assertion

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

Distinct variable group:   x,A

Proof of Theorem elex

Step	Hyp	Ref	Expression
1		elisset 1808	. 2 |- (A e. B -> A e. V)
2		isset 1805	. 2 |- (A e. V <-> E.x x = A)
3	1, 2	sylib 198	1 |- (A e. B -> E.x x = A)

Syntax hints:   -> wi 3   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802

This theorem is referenced by:  ceqsalg 1816  cgsexg 1822  cgsex2g 1823  cgsex4g 1824  vtocleg 1846  vtoclegft 1847  cla42egv 1855  cla43egv 1857  sbcel1gv 1970  sbcel2gv 1971  sbcgf 1976  copsex2g 2783  fvopab2 3776  fvopab5 3778  eloprabg 3992  nn1suc 5887  elo 10345

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain