Theorem fvopab4 4743

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

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

This theorem is referenced by:  fopabco 4805  funiunfv 4842  curry1 5075  curry1val 5077  curry2 5078  curry2val 5080  fvopabf4 5399  mapenlem1 5583  mapenlem2 5584  unfilem2 5642  aceq3lem 5894  aceq4 5896  aceq6a 5903  flval 7464  icoshftf1oii 7578  uzval 7588  seq1val2 7727  ser11i 7748  ser1p1i 7749  shftval 7759  seqzres2 7804  ser00i 7809  ser0p1i 7810  sqrval 7921  reval 8005  imval 8006  absval 8012  cjval 8013  fsump1i 8266  climsub 8390  climcmplem 8397  caucvg3i 8427  iserzabsi 8439  cvgcmp2i 8441  cvgcmp2ci 8444  cvgcmp3cei 8448  isummulc1 8473  isummulc1iALT 8474  infcvgi 8485  explecnv 8495  geolimilem 8497  geolimi 8498  geolim1i 8500  cvgratlem3ALT 8511  cvgratlem3 8514  cvgratlem5 8516  negfcncfi 8531  dsupivthlem 8553  efcltlem1 8566  dfef2i 8569  efval 8570  ef0lem 8572  efcl 8574  efcvg 8576  eftval 8578  erelem2 8582  erelem3 8583  erelem6 8586  ege2lem2 8590  ege2le3lem2 8591  efaddlem26 8625  efaddlem27 8626  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  eflegeolem2 8679  sinval 8694  cosval 8695  cnpval 9035  metcnp4lem1 9246  xplmi 9251  xplm 9253  xpcn 9254  bopcnlem2 9260  grplactval 9405  imsval 9648  vacnlem5 9671  sqcn 9674  va1cnlem 9684  sm1cnilem 9686  ip1cnilem4 9715  ip1cnilem6 9717  sspval 9721  hmoval 9810  ipasslem6 9836  ipasslem8 9838  ipasslem9 9839  ipblnfi 9857  ubthlem1 9872  ubthlem3 9874  minveclem23 9912  minveclem33 9922  minveceu 9928  htthlem3 9969  htthlem4 9970  efgh 10072  efghgrpilem 10073  efif 10075  efifo 10083  efif1 10091  shftefif1olem 10095  eff1i 10098  effoi 10099  upxp 10225  uptx 10226  txcnopab 10228  normval 10623  ocval 10786  occllem3 10808  projlem23 10841  pjmval 10871  hosval 11149  hosvalOLD 11150  homval 11151  hodval 11152  hodvalOLD 11153  hfsval 11154  hfmval 11155  braval 11504  bravalval 11505  kbvalval 11515  eigval1 11521  cnlnadjlem1 11637  cnlnadjlem4 11640  nmopadjlei 11658  strlem2 11823  hstrlem2 11831  cdj3lem2 12007  fprodp1i 14674  limfillem1 14938  idtrgrp 14978  ishoma 15136  ismona 15158  isepia 15168  cinvlem1 15176  cinvlem2 15177  issubcat 15193  upixp 15729  sdclem1 15809  fdc 15812  fsumltisumi 15823  mettrifi2 15848  geomcau 15849  lmclim2 15850  metdcn 15853  addccncf 15883  sub1cncf 15885  sub2cncf 15886  heiborlem2 15956  heiborlem3 15957  heiborlem33 15987  bfplem8 16005  rrnval 16013  rrnmet 16016  rrncms 16019  rrntotbndlem2 16021  ismrer1 16024  phtpyfval 16046  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpcval 16058  pcofval 16072  pcoval1 16074  pcoval2 16075  pcocn 16076  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorev 16087  pi1gp 16095  idlval 16161  pridlval 16181  maxidlval 16187  addrfv 16469  subrfv 16470  mulvfv 16471

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