Theorem moabex 2761

Description: "At most one" existence implies a class abstraction exists.

Assertion

Ref	Expression
moabex	|- (E*xph -> {x | ph} e. V)

Proof of Theorem moabex

Step	Hyp	Ref	Expression
1		ax-17 969	. . 3 |- (ph -> A.yph)
2	1	mo2 1398	. 2 |- (E*xph <-> E.yA.x(ph -> x = y))
3		hba1 1001	. . . . 5 |- (A.x(ph -> x = y) -> A.xA.x(ph -> x = y))
4		pm4.71 634	. . . . . . . 8 |- ((ph -> x = y) <-> (ph <-> (ph /\ x = y)))
5	4	biimp 151	. . . . . . 7 |- ((ph -> x = y) -> (ph <-> (ph /\ x = y)))
6	5	a4s 982	. . . . . 6 |- (A.x(ph -> x = y) -> (ph <-> (ph /\ x = y)))
7		ancom 435	. . . . . 6 |- ((ph /\ x = y) <-> (x = y /\ ph))
8	6, 7	syl6bb 535	. . . . 5 |- (A.x(ph -> x = y) -> (ph <-> (x = y /\ ph)))
9	3, 8	abbid 1573	. . . 4 |- (A.x(ph -> x = y) -> {x | ph} = {x | (x = y /\ ph)})
10		df-sn 2408	. . . . . 6 |- {y} = {x | x = y}
11		snex 2745	. . . . . 6 |- {y} e. V
12	10, 11	eqeltrr 1542	. . . . 5 |- {x | x = y} e. V
13		pm3.26 319	. . . . . 6 |- ((x = y /\ ph) -> x = y)
14	13	ss2abi 2116	. . . . 5 |- {x | (x = y /\ ph)} (_ {x | x = y}
15	12, 14	ssexi 2715	. . . 4 |- {x | (x = y /\ ph)} e. V
16	9, 15	syl6eqel 1553	. . 3 |- (A.x(ph -> x = y) -> {x | ph} e. V)
17	16	19.23aiv 1293	. 2 |- (E.yA.x(ph -> x = y) -> {x | ph} e. V)
18	2, 17	sylbi 199	1 |- (E*xph -> {x | ph} e. V)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978  E*wmo 1379  {cab 1461  Vcvv 1807  {csn 2405

This theorem is referenced by:  euabex 2762  fvex 3723  supex 4557

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408

Copyright terms: Public domain