Metamath Proof Explorer

Theorem maprnin

Description: Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017)

Ref Expression
Hypotheses maprnin.1 ⊢A∈V
maprnin.2 ⊢B∈V
Assertion maprnin ⊢B∩CA=f∈BA|ran⁡f⊆C

Proof

Step Hyp Ref Expression
1 maprnin.1 ⊢A∈V
2 maprnin.2 ⊢B∈V
3 ffn ⊢f:A⟶B→fFnA
4 df-f ⊢f:A⟶C↔fFnA∧ran⁡f⊆C
5 4 baibr ⊢fFnA→ran⁡f⊆C↔f:A⟶C
6 3 5 syl ⊢f:A⟶B→ran⁡f⊆C↔f:A⟶C
7 6 pm5.32i ⊢f:A⟶B∧ran⁡f⊆C↔f:A⟶B∧f:A⟶C
8 2 1 elmap ⊢f∈BA↔f:A⟶B
9 8 anbi1i ⊢f∈BA∧ran⁡f⊆C↔f:A⟶B∧ran⁡f⊆C
10 fin ⊢f:A⟶B∩C↔f:A⟶B∧f:A⟶C
11 7 9 10 3bitr4ri ⊢f:A⟶B∩C↔f∈BA∧ran⁡f⊆C
12 11 abbii ⊢f|f:A⟶B∩C=f|f∈BA∧ran⁡f⊆C
13 2 inex1 ⊢B∩C∈V
14 13 1 mapval ⊢B∩CA=f|f:A⟶B∩C
15 df-rab ⊢f∈BA|ran⁡f⊆C=f|f∈BA∧ran⁡f⊆C
16 12 14 15 3eqtr4i ⊢B∩CA=f∈BA|ran⁡f⊆C