# Metamath Proof Explorer

## Theorem dff4

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dff4 ${⊢}{F}:{A}⟶{B}↔\left({F}\subseteq {A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$

### Proof

Step Hyp Ref Expression
1 dff3 ${⊢}{F}:{A}⟶{B}↔\left({F}\subseteq {A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
2 df-br ${⊢}{x}{F}{y}↔⟨{x},{y}⟩\in {F}$
3 ssel ${⊢}{F}\subseteq {A}×{B}\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in \left({A}×{B}\right)\right)$
4 opelxp2 ${⊢}⟨{x},{y}⟩\in \left({A}×{B}\right)\to {y}\in {B}$
5 3 4 syl6 ${⊢}{F}\subseteq {A}×{B}\to \left(⟨{x},{y}⟩\in {F}\to {y}\in {B}\right)$
6 2 5 syl5bi ${⊢}{F}\subseteq {A}×{B}\to \left({x}{F}{y}\to {y}\in {B}\right)$
7 6 pm4.71rd ${⊢}{F}\subseteq {A}×{B}\to \left({x}{F}{y}↔\left({y}\in {B}\wedge {x}{F}{y}\right)\right)$
8 7 eubidv ${⊢}{F}\subseteq {A}×{B}\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {x}{F}{y}\right)\right)$
9 df-reu ${⊢}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {x}{F}{y}\right)$
10 8 9 syl6bbr ${⊢}{F}\subseteq {A}×{B}\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}↔\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
11 10 ralbidv ${⊢}{F}\subseteq {A}×{B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
12 11 pm5.32i ${⊢}\left({F}\subseteq {A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)↔\left({F}\subseteq {A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
13 1 12 bitri ${⊢}{F}:{A}⟶{B}↔\left({F}\subseteq {A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$