Theorem fvopab2 3776

Description: Value of a function given by an ordered-pair class abstraction.

Assertion

Ref	Expression
fvopab2	|- ((x e. A /\ B e. C) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B)

Distinct variable groups:   y,A   y,B   x,y

Proof of Theorem fvopab2

Step	Hyp	Ref	Expression
1		elex 1810	. . 3 |- (B e. C -> E.y y = B)
2		ax-17 968	. . . . 5 |- (x e. A -> A.y x e. A)
3		hbopab2 2803	. . . . . . 7 |- (z e. {<.x, y>. | (x e. A /\ y = B)} -> A.y z e. {<.x, y>. | (x e. A /\ y = B)})
4		ax-17 968	. . . . . . 7 |- (z e. x -> A.y z e. x)
5	3, 4	hbfv 3714	. . . . . 6 |- (z e. ({<.x, y>. | (x e. A /\ y = B)}` x) -> A.y z e. ({<.x, y>. | (x e. A /\ y = B)}` x))
6		ax-17 968	. . . . . 6 |- (z e. B -> A.y z e. B)
7	5, 6	hbeq 1557	. . . . 5 |- (({<.x, y>. | (x e. A /\ y = B)}` x) = B -> A.y({<.x, y>. | (x e. A /\ y = B)}` x) = B)
8	2, 7	hbim 1004	. . . 4 |- ((x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B) -> A.y(x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B))
9		visset 1804	. . . . . . . 8 |- y e. V
10		eleq1 1526	. . . . . . . 8 |- (y = B -> (y e. V <-> B e. V))
11	9, 10	mpbii 193	. . . . . . 7 |- (y = B -> B e. V)
12	3	tz6.12f 3723	. . . . . . . . . . 11 |- ((<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)} /\ E!y<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)}) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y)
13		opabid 2799	. . . . . . . . . . 11 |- (<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)} <-> (x e. A /\ y = B))
14	12, 13	sylanbr 450	. . . . . . . . . 10 |- (((x e. A /\ y = B) /\ E!y<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)}) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y)
15		euanv 1425	. . . . . . . . . . 11 |- (E!y(x e. A /\ y = B) <-> (x e. A /\ E!y y = B))
16	13	eubii 1380	. . . . . . . . . . 11 |- (E!y<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)} <-> E!y(x e. A /\ y = B))
17		eueq 1907	. . . . . . . . . . . 12 |- (B e. V <-> E!y y = B)
18	17	anbi2i 479	. . . . . . . . . . 11 |- ((x e. A /\ B e. V) <-> (x e. A /\ E!y y = B))
19	15, 16, 18	3bitr4r 184	. . . . . . . . . 10 |- ((x e. A /\ B e. V) <-> E!y<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)})
20	14, 19	sylan2b 452	. . . . . . . . 9 |- (((x e. A /\ y = B) /\ (x e. A /\ B e. V)) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y)
21	20	exp43 384	. . . . . . . 8 |- (x e. A -> (y = B -> (x e. A -> (B e. V -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y))))
22	21	pm2.43a 66	. . . . . . 7 |- (x e. A -> (y = B -> (B e. V -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y)))
23	11, 22	mpdi 48	. . . . . 6 |- (x e. A -> (y = B -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y))
24	23	com12 11	. . . . 5 |- (y = B -> (x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = y))
25		eqeq2 1476	. . . . 5 |- (y = B -> (({<.x, y>. | (x e. A /\ y = B)}` x) = y <-> ({<.x, y>. | (x e. A /\ y = B)}` x) = B))
26	24, 25	sylibd 202	. . . 4 |- (y = B -> (x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B))
27	8, 26	19.23ai 1060	. . 3 |- (E.y y = B -> (x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B))
28	1, 27	syl 10	. 2 |- (B e. C -> (x e. A -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B))
29	28	impcom 351	1 |- ((x e. A /\ B e. C) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  E!weu 1373  Vcvv 1802  <.cop 2401  {copab 2656  ` cfv 3172

This theorem is referenced by:  elrnopabg 3785  fopab2 3808  rnssopab 3810  fopabco 3817  fopabsn 3825  abrexexlem2 3844  dom2d 4385  pw2en 4426  mapxpen 4475  xpmapenlem2 4477  xpmapenlem4 4479  xpmapenlem5 4480  ac6lem 4726  iundom 4784  sumeqfv 6935  serzfsum 6942  fsum1 6943  fsump1 6944  isumval2t 7130  isumclim3t 7135  isumcmpi 7150  geoisum1c 7180  fsumcnlem 7923  cnlnadjlem5 9919  fvopab2a 10359

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188

Copyright terms: Public domain