Theorem fvopab4 3765

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

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  Vcvv 1802  {copab 2656  ` cfv 3172

This theorem is referenced by:  fopabco 3817  funiunfv 3851  curry1 4082  curry1val 4084  fvopabf4 4324  mapenlem1 4469  mapenlem2 4470  unfilem2 4525  aceq3lem 4704  aceq4 4706  aceq6a 4713  flvalt 6173  seq1val2 6251  ser11 6272  ser1p1 6273  shftvalt 6283  icoshftf1oi 6342  uzvalt 6351  seqzres2 6493  ser00 6498  ser0p1 6499  sqrval 6601  revalt 6686  imvalt 6687  absvalt 6694  cjvalt 6695  fsump1 6944  climsub 7066  climcmplem 7073  caucvg3 7103  iserzabs 7115  cvgcmp2 7117  cvgcmp2c 7119  cvgcmp3ce 7123  isummulc1 7147  isummulc1ALT 7148  infcvg 7159  geolimilem 7170  geolimi 7171  geolim1i 7173  cvgratlem3ALT 7184  cvgratlem3 7187  cvgratlem5 7189  negfcncf 7204  dsupivthlem 7226  efcltlem1 7246  dfef2 7249  efvalt 7250  ef0lem 7252  efclt 7254  efcvg 7256  eftval 7258  erelem2 7262  erelem3 7263  erelem6 7266  ege2lem2 7270  ege2le3lem2 7271  efaddlem26 7305  efaddlem27 7306  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  eflegeolem2 7354  sinvalt 7371  cosvalt 7372  cnpval 7699  metcnp4lem1 7902  xplmi 7907  xplm 7909  xpcn 7910  bopcnlem2 7916  grplactval 8033  imsval 8254  sqcn 8270  va1cnlem 8279  sm1cnilem 8281  ip1cnilem4 8310  ip1cnilem6 8312  sspval 8316  hmoval 8401  ipasslem6 8426  ipasslem8 8428  ipasslem9 8429  ipblnfi 8447  ubthlem1 8460  ubthlem3 8462  minveclem23 8498  minveclem33 8508  minveceu 8514  htthlem3 8552  htthlem4 8553  efgh 8633  efghgrpilem 8634  efif 8636  efifo 8644  efif1 8652  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  effoi 8666  effoiOLD 8667  normvalt 8911  ocvalt 9069  occllem3 9091  projlem23 9124  pjmvalt 9153  hosvalt 9433  hosvaltOLD 9434  homvalt 9435  hodvalt 9436  hodvaltOLD 9437  hfsvalt 9438  hfmvalt 9439  bravalt 9783  bravalvalt 9784  kbvalvalt 9794  eigvalt 9800  cnlnadjlem1 9915  cnlnadjlem4 9918  nmopadjle 9936  strlem2 10088  hstrlem2 10096  cdj3lem2 10267  ishoma 10559  ismona 10579

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-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fv 3188

Copyright terms: Public domain