Theorem elex 1816

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 1814	. 2 |- (A e. B -> A e. V)
2		isset 1811	. 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 955   e. wcel 957  E.wex 979  Vcvv 1808

This theorem is referenced by:  ceqsalg 1822  cgsexg 1828  cgsex2g 1829  cgsex4g 1830  vtocleg 1852  vtoclegft 1853  cla42egv 1861  cla43egv 1863  sbcel1gv 1977  sbcel2gv 1978  sbcgf 1983  copsex2g 2789  fvopab2 3786  fvopab5 3788  eloprabg 4002  nn1suc 5897  elo 10403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain