Metamath Proof Explorer


Theorem dff4

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

Ref Expression
Assertion dff4 F : A B F A × B x A ∃! y B x F y

Proof

Step Hyp Ref Expression
1 dff3 F : A B F A × B x A ∃! y x F y
2 df-br x F y x y F
3 ssel F A × B x y F x y A × B
4 opelxp2 x y A × B y B
5 3 4 syl6 F A × B x y F y B
6 2 5 syl5bi F A × B x F y y B
7 6 pm4.71rd F A × B x F y y B x F y
8 7 eubidv F A × B ∃! y x F y ∃! y y B x F y
9 df-reu ∃! y B x F y ∃! y y B x F y
10 8 9 bitr4di F A × B ∃! y x F y ∃! y B x F y
11 10 ralbidv F A × B x A ∃! y x F y x A ∃! y B x F y
12 11 pm5.32i F A × B x A ∃! y x F y F A × B x A ∃! y B x F y
13 1 12 bitri F : A B F A × B x A ∃! y B x F y