fvmpt2d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fvmpt2d		Structured version Visualization version GIF version

Theorem fvmpt2d 7012

Description: Deduction version of fvmpt2 7010. (Contributed by Thierry Arnoux, 8-Dec-2016.)

**Hypotheses**
Ref	Expression
fvmpt2d.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
fvmpt2d.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)

**Assertion**
Ref	Expression
fvmpt2d	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Distinct variable group: 𝑥,𝐴 Allowed substitution hints: 𝜑(𝑥) 𝐵(𝑥) 𝐹(𝑥) 𝑉(𝑥)

**Proof of Theorem fvmpt2d**
Step	Hyp	Ref	Expression
1		fvmpt2d.1	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
2	1	fveq1d 6893	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2728	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 7010	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 685	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2768	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ↦ cmpt 5225 ‘cfv 6542

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pr 5423

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fv 6550

This theorem is referenced by: cantnflem1 9706 ghmquskerco 19228 frlmphl 21708 neiptopreu 23030 rrxds 25314 ofoprabco 32443 suppovss 32458 tocycf 32832 ply1moneq 33254 fedgmullem2 33318 esumcvg 33699 ofcfval2 33717 eulerpartgbij 33986 dstrvprob 34085 itgexpif 34232 hgt750lemb 34282 aks6d1c6lem4 41639 frlmsnic 41764 cvgdvgrat 43744 radcnvrat 43745 binomcxplemnotnn0 43787 fmuldfeqlem1 44964 climreclmpt 45066 climinfmpt 45097 limsupubuzmpt 45101 limsupre2mpt 45112 limsupre3mpt 45116 limsupreuzmpt 45121 liminfvalxrmpt 45168 liminflbuz2 45197 cncficcgt0 45270 dvdivbd 45305 dvnmul 45325 dvnprodlem1 45328 dvnprodlem2 45329 stoweidlem42 45424 dirkeritg 45484 elaa2lem 45615 etransclem4 45620 ioorrnopnxrlem 45688 subsaliuncllem 45739 meaiuninclem 45862 meaiininclem 45868 ovnhoilem1 45983 ovncvr2 45993 ovolval4lem1 46031 iccvonmbllem 46060 vonioolem1 46062 vonioolem2 46063 vonicclem1 46065 vonicclem2 46066 pimconstlt0 46083 pimconstlt1 46084 smfpimltmpt 46128 issmfdmpt 46130 smfaddlem2 46146 smflimlem2 46154 smflimlem4 46156 smfpimgtmpt 46163 smfmullem4 46176 smfpimcclem 46189 smfsuplem1 46193 smfsupmpt 46197 smfinfmpt 46201 smflimsuplem2 46203 smflimsuplem3 46204 smflimsuplem4 46205 fsupdm 46224 finfdm 46228

	
		OSZAR »