Theorem elex 1819

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 1817	. 2 |- (A e. B -> A e. V)
2		isset 1814	. 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 956   e. wcel 958  E.wex 980  Vcvv 1811

This theorem is referenced by:  ceqsalg 1825  cgsexg 1831  cgsex2g 1832  cgsex4g 1833  vtocleg 1855  vtoclegft 1856  cla42egv 1864  cla43egv 1866  sbcel1gv 1980  sbcel2gv 1981  sbcgf 1986  copsex2g 2793  fvopab2 3791  fvopab5 3793  eloprabg 4007  nn1suc 5939  elo 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain