Theorem ceqsex3OLD 16249

Description: Version of ceqsex 2324 with an antecedent instead of a hypothesis. (Use ceqsexg 2392 instead of this one. --NM 13-Aug-11)

Hypotheses

Ref	Expression
ceqsex3.1OLD	|- (ps -> A.xps)
ceqsex3.2OLD	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
ceqsex3OLD	|- (A e. _V -> (E.x(x = A /\ ph) <-> ps))

Distinct variable group:   x,A

Proof of Theorem ceqsex3OLD

Step	Hyp	Ref	Expression
1		ceqsex3.1OLD	. . 3 |- (ps -> A.xps)
2		ceqsex3.2OLD	. . . 4 |- (x = A -> (ph <-> ps))
3	2	biimpa 460	. . 3 |- ((x = A /\ ph) -> ps)
4	1, 3	19.23ai 1412	. 2 |- (E.x(x = A /\ ph) -> ps)
5	2	biimprcd 173	. . . . . 6 |- (ps -> (x = A -> ph))
6	1, 5	19.21ai 1345	. . . . 5 |- (ps -> A.x(x = A -> ph))
7		exintr 1475	. . . . 5 |- (A.x(x = A -> ph) -> (E.x x = A -> E.x(x = A /\ ph)))
8	6, 7	syl 12	. . . 4 |- (ps -> (E.x x = A -> E.x(x = A /\ ph)))
9		isset 2296	. . . 4 |- (A e. _V <-> E.x x = A)
10	8, 9	syl5ib 223	. . 3 |- (ps -> (A e. _V -> E.x(x = A /\ ph)))
11	10	com12 14	. 2 |- (A e. _V -> (ps -> E.x(x = A /\ ph)))
12	4, 11	impbid2 576	1 |- (A e. _V -> (E.x(x = A /\ ph) <-> ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain