Theorem fvopab2 3730

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 1794	. . 3 |- (B e. C -> E.y y = B)
2		ax-17 1190	. . . . 5 |- (x e. A -> A.y x e. A)
3		hbopab2 2776	. . . . . . 7 |- (z e. {<.x, y>. | (x e. A /\ y = B)} -> A.y z e. {<.x, y>. | (x e. A /\ y = B)})
4		ax-17 1190	. . . . . . 7 |- (z e. x -> A.y z e. x)
5	3, 4	hbfv 3668	. . . . . 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 1190	. . . . . 6 |- (z e. B -> A.y z e. B)
7	5, 6	hbeq 1541	. . . . 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 983	. . . 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 1788	. . . . . . . 8 |- y e. V
10		eleq1 1510	. . . . . . . 8 |- (y = B -> (y e. V <-> B e. V))
11	9, 10	mpbii 193	. . . . . . 7 |- (y = B -> B e. V)
12	3	tz6.12f 3677	. . . . . . . . . . 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 2772	. . . . . . . . . . 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 1409	. . . . . . . . . . 11 |- (E!y(x e. A /\ y = B) <-> (x e. A /\ E!y y = B))
16	13	eubii 1364	. . . . . . . . . . 11 |- (E!y<.x, y>. e. {<.x, y>. | (x e. A /\ y = B)} <-> E!y(x e. A /\ y = B))
17		eueq 1888	. . . . . . . . . . . 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 1460	. . . . 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 1040	. . 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  E.wex 956   = wceq 1099   e. wcel 1105  E!weu 1357  Vcvv 1786  <.cop 2382  {copab 2634  ` cfv 3145

This theorem is referenced by:  elrnopabg 3739  fopab2 3762  rnssopab 3764  fopabco 3771  fopabsn 3779  abrexexlem2 3798  dom2d 4339  pw2en 4380  mapxpen 4427  xpmapenlem2 4429  xpmapenlem4 4431  xpmapenlem5 4432  ac6lem 4678  iundom 4736  sumeqfv 6886  serzfsum 6893  fsum1 6894  fsump1 6895  isumval2t 7081  isumclim3t 7086  isumcmpi 7101  geoisum1c 7131  fsumcnlem 7871  fvopab2a 8718  cnlnadjlem5 10133

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161

Copyright terms: Public domain