Theorem fvopab4 3775

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 3774	. 2 |- ((A e. D /\ C e. V) -> (F` A) = C)
5	1, 4	mpan2 695	1 |- (A e. D -> (F` A) = C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  Vcvv 1808  {copab 2662  ` cfv 3178

This theorem is referenced by:  fopabco 3827  funiunfv 3861  curry1 4091  curry1val 4093  fvopabf4 4333  mapenlem1 4478  mapenlem2 4479  unfilem2 4534  aceq3lem 4715  aceq4 4717  aceq6a 4724  flvalt 6183  seq1val2 6264  ser11 6285  ser1p1 6286  shftvalt 6296  icoshftf1oi 6355  uzvalt 6364  seqzres2 6506  ser00 6511  ser0p1 6512  sqrval 6616  revalt 6701  imvalt 6702  absvalt 6709  cjvalt 6710  fsump1 6959  climsub 7083  climcmplem 7090  caucvg3 7120  iserzabs 7132  cvgcmp2 7134  cvgcmp2c 7136  cvgcmp3ce 7140  isummulc1 7164  isummulc1ALT 7165  infcvg 7176  geolimilem 7187  geolimi 7188  geolim1i 7190  cvgratlem3ALT 7201  cvgratlem3 7204  cvgratlem5 7206  negfcncf 7221  dsupivthlem 7243  efcltlem1 7263  dfef2 7266  efvalt 7267  ef0lem 7269  efclt 7271  efcvg 7273  eftval 7275  erelem2 7279  erelem3 7280  erelem6 7283  ege2lem2 7287  ege2le3lem2 7288  efaddlem26 7322  efaddlem27 7323  ef1tllem 7340  ef01tllem1 7342  ef01tllem2 7343  eflegeolem2 7371  sinvalt 7388  cosvalt 7389  cnpval 7719  metcnp4lem1 7930  xplmi 7935  xplm 7937  xpcn 7938  bopcnlem2 7944  grplactval 8060  imsval 8280  sqcn 8298  va1cnlem 8307  sm1cnilem 8309  ip1cnilem4 8338  ip1cnilem6 8340  sspval 8344  hmoval 8429  ipasslem6 8454  ipasslem8 8456  ipasslem9 8457  ipblnfi 8475  ubthlem1 8488  ubthlem3 8490  minveclem23 8526  minveclem33 8536  minveceu 8542  htthlem3 8580  htthlem4 8581  efgh 8668  efghgrpilem 8669  efif 8671  efifo 8679  efif1 8687  shftefif1olem 8696  eff1i 8699  effoi 8700  normvalt 8945  ocvalt 9108  occllem3 9130  projlem23 9163  pjmvalt 9193  hosvalt 9473  hosvaltOLD 9474  homvalt 9475  hodvalt 9476  hodvaltOLD 9477  hfsvalt 9478  hfmvalt 9479  bravalt 9824  bravalvalt 9825  kbvalvalt 9835  eigvalt 9841  cnlnadjlem1 9956  cnlnadjlem4 9959  nmopadjle 9977  strlem2 10134  hstrlem2 10142  cdj3lem2 10318  limfillem1 10523  ishoma 10631  ismona 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-id 2831  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fv 3194

Copyright terms: Public domain