This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∩ C A = f ∈ B A | ran ⁡ f ⊆ C

Proof

Step Hyp Ref Expression
1 maprnin.1 ⊢ A ∈ V
2 maprnin.2 ⊢ B ∈ V
3 ffn ⊢ f : A ⟶ B → f Fn A
4 df-f ⊢ f : A ⟶ C ↔ f Fn A ∧ ran ⁡ f ⊆ C
5 4 baibr ⊢ f Fn A → 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 ∈ B A ↔ f : A ⟶ B
9 8 anbi1i ⊢ f ∈ B A ∧ 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 ∈ B A ∧ ran ⁡ f ⊆ C
12 11 abbii ⊢ f | f : A ⟶ B ∩ C = f | f ∈ B A ∧ ran ⁡ f ⊆ C
13 2 inex1 ⊢ B ∩ C ∈ V
14 13 1 mapval ⊢ B ∩ C A = f | f : A ⟶ B ∩ C
15 df-rab ⊢ f ∈ B A | ran ⁡ f ⊆ C = f | f ∈ B A ∧ ran ⁡ f ⊆ C
16 12 14 15 3eqtr4i ⊢ B ∩ C A = f ∈ B A | ran ⁡ f ⊆ C