Theorem fvmpt3i 6996

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypotheses

Ref	Expression
fvmpt3.a	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmpt3.b	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmpt3i.c	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fvmpt3i	⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt3i

Step	Hyp	Ref	Expression
1		fvmpt3.a	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
2		fvmpt3.b	. 2 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
3		fvmpt3i.c	. . 3 ⊢ 𝐵 ∈ V
4	3	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ V)
5	1, 2, 4	fvmpt3 6995	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ↦ cmpt 5196  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is referenced by:  isf32lem9  10345  axcc2lem  10420  caucvg  15730  ismre  17642  mrisval  17686  frmdup1  18923  frmdup2  18924  qusghm  19325  pmtrfval  19520  odf1  19632  vrgpfval  19836  dprdz  20102  dmdprdsplitlem  20109  dprd2dlem2  20112  dprd2dlem1  20113  dprd2da  20114  ablfac1a  20141  ablfac1b  20142  ablfac1eu  20145  ipdir  21758  ipass  21764  isphld  21773  istopon  23038  qustgpopn  24246  qustgplem  24247  tcphcph  25365  cmvth  26119  mvth  26120  dvle  26135  lhop1  26142  dvfsumlem3  26156  pige3ALT  26651  fsumdvdscom  27315  logfacbnd3  27353  dchrptlem1  27394  dchrptlem2  27395  lgsdchrval  27484  dchrisumlem3  27621  dchrisum0flblem1  27638  dchrisum0fno1  27641  dchrisum0lem1b  27645  dchrisum0lem2a  27647  dchrisum0lem2  27648  logsqvma2  27673  log2sumbnd  27674  zringfrac  33789  measdivcst  34559  measdivcstALTV  34560  mrexval  35892  mexval  35893  mdvval  35895  msubvrs  35951  mthmval  35966  weiunlem  36863  f1omptsnlem  37870  upixp  38268  ismrer1  38377  frlmsnic  43200  fsuppind  43214  uzmptshftfval  44948  tposideq  49551  fucocolem2  50017  amgmwlem  50476  amgmlemALT  50477