Theorem fvopab4g 4742

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

Hypotheses

Ref	Expression
fvopab4g.1	|- (x = A -> B = C)
fvopab4g.2	|- F = {<.x, y>. | (x e. D /\ y = B)}

Assertion

Ref	Expression
fvopab4g	|- ((A e. D /\ C e. R) -> (F` A) = C)

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

Proof of Theorem fvopab4g

Step	Hyp	Ref	Expression
1		eqid 1884	. 2 |- C = C
2		fvopab4g.1	. . . 4 |- (x = A -> B = C)
3	2	eqeq2d 1895	. . 3 |- (x = A -> (y = B <-> y = C))
4		eqeq1 1890	. . 3 |- (y = C -> (y = C <-> C = C))
5		moeq 2431	. . . 4 |- E*y y = B
6	5	a1i 8	. . 3 |- (x e. D -> E*y y = B)
7		fvopab4g.2	. . 3 |- F = {<.x, y>. | (x e. D /\ y = B)}
8	3, 4, 6, 7	fvopab3ig 4741	. 2 |- ((A e. D /\ C e. R) -> (C = C -> (F` A) = C))
9	1, 8	mpi 55	1 |- ((A e. D /\ C e. R) -> (F` A) = C)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E*wmo 1772  {copab 3395  ` cfv 3998

This theorem is referenced by:  fvopab4 4743  fvopab4gf 4744  fvopabg 4748  fvmptg 5014  cfval 6054  fsum1i 8265  mulc1cncf 8541  tgval 8886  cldval 8942  ntrfval 8943  clsfval 8944  ntrval 8952  clsval 8953  neifval 8990  neival 8993  lpfval 9018  lpval 9019  blfval 9112  opnfval 9134  lmfval 9203  caufval 9204  lmfexlem2 9235  grpidvallem 9341  grpinvfval 9350  grpinvval 9351  grpdivfval 9366  gxoprval 9380  grplactfval 9404  issubg 9425  sincolem 10014  oprabco 10159  fiv 10212  fgf 10283  sfvlim 10296  idrval 10374  pjval 10872  spanval 10932  hsupval2 10933  eucalgval 13749  valpr 14499  prjmapcp2 14515  iscst1 14519  valcurfn1 14552  valvalcurfn 14554  mxlelt2 14606  mxlelt 14607  mnlelt2 14608  fprod1i 14673  curgrpact 14735  homcard 14893  cntrsetlem 14999  cnvtr 15016  trclval 15271  isline1 15294  upixp 15729  sdc 15811  tlmval 15903

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fv 4014

Copyright terms: Public domain