Metamath Proof Explorer

Theorem mapval2

Description: Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007)

Ref Expression
Hypotheses elmap.1 ⊢ A ∈ V
elmap.2 ⊢ B ∈ V
Assertion mapval2 ⊢ A B = 𝒫 B × A ∩ f | f Fn B

Proof

Step Hyp Ref Expression
1 elmap.1 ⊢ A ∈ V
2 elmap.2 ⊢ B ∈ V
3 dff2 ⊢ g : B ⟶ A ↔ g Fn B ∧ g ⊆ B × A
4 3 biancomi ⊢ g : B ⟶ A ↔ g ⊆ B × A ∧ g Fn B
5 1 2 elmap ⊢ g ∈ A B ↔ g : B ⟶ A
6 elin ⊢ g ∈ 𝒫 B × A ∩ f | f Fn B ↔ g ∈ 𝒫 B × A ∧ g ∈ f | f Fn B
7 velpw ⊢ g ∈ 𝒫 B × A ↔ g ⊆ B × A
8 vex ⊢ g ∈ V
9 fneq1 ⊢ f = g → f Fn B ↔ g Fn B
10 8 9 elab ⊢ g ∈ f | f Fn B ↔ g Fn B
11 7 10 anbi12i ⊢ g ∈ 𝒫 B × A ∧ g ∈ f | f Fn B ↔ g ⊆ B × A ∧ g Fn B
12 6 11 bitri ⊢ g ∈ 𝒫 B × A ∩ f | f Fn B ↔ g ⊆ B × A ∧ g Fn B
13 4 5 12 3bitr4i ⊢ g ∈ A B ↔ g ∈ 𝒫 B × A ∩ f | f Fn B
14 13 eqriv ⊢ A B = 𝒫 B × A ∩ f | f Fn B