Theorem fvopab4 3856

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)}
fvopab4.3	|- C e. V

Assertion

Ref	Expression
fvopab4	|- (A e. D -> (F` A) = C)

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

Proof of Theorem fvopab4

Step	Hyp	Ref	Expression
1		fvopab4.3	. 2 |- C e. V
2		fvopab4g.1	. . 3 |- (x = A -> B = C)
3		fvopab4g.2	. . 3 |- F = {<.x, y>. | (x e. D /\ y = B)}
4	2, 3	fvopab4g 3855	. 2 |- ((A e. D /\ C e. V) -> (F` A) = C)
5	1, 4	mpan2 699	1 |- (A e. D -> (F` A) = C)

Syntax hints:   -> wi 3   /\ wa 221   = wceq 988   e. wcel 990  Vcvv 1849  {copab 2717  ` cfv 3237

This theorem is referenced by:  fopabco 3908  funiunfv 3942  curry1 4208  curry1val 4210  curry2 4211  fvopabf4 4427  mapenlem1 4578  mapenlem2 4579  unfilem2 4636  aceq3lem 4818  aceq4 4820  aceq6a 4827  flval 6364  icoshftf1oii 6469  uzval 6479  seq1val2 6607  ser11i 6628  ser1p1i 6629  shftval 6639  seqzres2 6684  ser00i 6689  ser0p1i 6690  sqrval 6794  reval 6878  imval 6879  absval 6885  cjval 6886  fsump1i 7129  climsub 7253  climcmplem 7260  caucvg3i 7290  iserzabsi 7302  cvgcmp2i 7304  cvgcmp2ci 7306  cvgcmp3cei 7310  isummulc1 7335  isummulc1iALT 7336  infcvgi 7347  geolimilem 7358  geolimi 7359  geolim1i 7361  cvgratlem3ALT 7372  cvgratlem3 7375  cvgratlem5 7377  negfcncfi 7392  dsupivthlem 7414  efcltlem1 7427  dfef2i 7430  efval 7431  ef0lem 7433  efcl 7435  efcvg 7437  eftval 7439  erelem2 7443  erelem3 7444  erelem6 7447  ege2lem2 7451  ege2le3lem2 7452  efaddlem26 7486  efaddlem27 7487  ef1tllem 7504  ef01tllem1 7506  ef01tllem2 7507  ef01tllem2OLD 7508  eflegeolem2 7538  sinval 7553  cosval 7554  cnpval 7879  metcnp4lem1 8088  xplmi 8093  xplm 8095  xpcn 8096  bopcnlem2 8102  grplactval 8216  imsval 8435  sqcn 8454  va1cnlem 8464  sm1cnilem 8466  ip1cnilem4 8495  ip1cnilem6 8497  sspval 8501  hmoval 8589  ipasslem6 8614  ipasslem8 8616  ipasslem9 8617  ipblnfi 8635  ubthlem1 8648  ubthlem3 8650  minveclem23 8686  minveclem33 8696  minveceu 8702  htthlem3 8741  htthlem4 8742  efgh 8837  efghgrpilem 8838  efif 8840  efifo 8848  efif1 8856  shftefif1olem 8860  eff1i 8863  effoi 8864  normval 9110  ocval 9273  occllem3 9295  projlem23 9328  pjmval 9358  hosval 9636  hosvalOLD 9637  homval 9638  hodval 9639  hodvalOLD 9640  hfsval 9641  hfmval 9642  braval 9985  bravalval 9986  kbvalval 9996  eigval1 10002  cnlnadjlem1 10117  cnlnadjlem4 10120  nmopadjlei 10138  strlem2 10296  hstrlem2 10304  cdj3lem2 10480  limfillem1OLD 10731  ishoma 10850  ismona 10872  isepia 10882  cinvlem1 10890  cinvlem2 10891

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fv 3253

Copyright terms: Public domain