Theorem elex 1356

Description: An element of a class exists.

Assertion

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

Distinct variable group(s):   x,A

Proof of Theorem elex

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

Syntax hints:   -> wi 2  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  ceqsalg 1362  cgsex2g 1368  cgsex4g 1369  vtocleg 1390  cla4e2gv 1398  sbcel1 1466  sbcel2 1467  sbcgf 1469  copsex2g 1903  opelopabg 2115  fvopab2 2878  eloprabg 3035  nn1suc 4435

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org