Theorem iota2df 4365

Description: A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)

Hypotheses

Ref	Expression
iota2df.1	|- (ph -> B e. V)
iota2df.2	|- (ph -> E!xps)
iota2df.3	|- ((ph /\ x = B) -> (ps <-> ch))
iota2df.4	|- F/xph
iota2df.5	|- (ph -> F/xch)
iota2df.6	|- (ph -> F/_xB)

Assertion

Ref	Expression
iota2df	|- (ph -> (ch <-> (iotaxps) = B))

Proof of Theorem iota2df

Step	Hyp	Ref	Expression
1		iota2df.6	. 2 |- (ph -> F/_xB)
2		iota2df.5	. . 3 |- (ph -> F/xch)
3		nfiota1 4341	. . . . 5 |- F/_x(iotaxps)
4	3	a1i 10	. . . 4 |- (ph -> F/_x(iotaxps))
5	4, 1	nfeqd 2503	. . 3 |- (ph -> F/x(iotaxps) = B)
6	2, 5	nfbid 1832	. 2 |- (ph -> F/x(ch <-> (iotaxps) = B))
7		iota2df.4	. . 3 |- F/xph
8		iota2df.3	. . . . 5 |- ((ph /\ x = B) -> (ps <-> ch))
9		simpr 447	. . . . . 6 |- ((ph /\ x = B) -> x = B)
10	9	eqeq2d 2364	. . . . 5 |- ((ph /\ x = B) -> ((iotaxps) = x <-> (iotaxps) = B))
11	8, 10	bibi12d 312	. . . 4 |- ((ph /\ x = B) -> ((ps <-> (iotaxps) = x) <-> (ch <-> (iotaxps) = B)))
12	11	ex 423	. . 3 |- (ph -> (x = B -> ((ps <-> (iotaxps) = x) <-> (ch <-> (iotaxps) = B))))
13	7, 12	alrimi 1765	. 2 |- (ph -> A.x(x = B -> ((ps <-> (iotaxps) = x) <-> (ch <-> (iotaxps) = B))))
14		iota2df.2	. . . 4 |- (ph -> E!xps)
15		iota1 4353	. . . 4 |- (E!xps -> (ps <-> (iotaxps) = x))
16	14, 15	syl 15	. . 3 |- (ph -> (ps <-> (iotaxps) = x))
17	7, 16	alrimi 1765	. 2 |- (ph -> A.x(ps <-> (iotaxps) = x))
18		iota2df.1	. 2 |- (ph -> B e. V)
19		vtoclgft 2905	. 2 |- ((( F/_xB /\ F/x(ch <-> (iotaxps) = B)) /\ (A.x(x = B -> ((ps <-> (iotaxps) = x) <-> (ch <-> (iotaxps) = B))) /\ A.x(ps <-> (iotaxps) = x)) /\ B e. V) -> (ch <-> (iotaxps) = B))
20	1, 6, 13, 17, 18, 19	syl221anc 1193	1 |- (ph -> (ch <-> (iotaxps) = B))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540   F/wnf 1544   = wceq 1642   e. wcel 1710  E!weu 2204   F/_wnfc 2476  iotacio 4337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-un 3214  df-sn 3741  df-pr 3742  df-uni 3892  df-iota 4339

This theorem is referenced by:  iota2d  4366  iota2  4367