Theorem dff4

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

	Ref	Expression
Assertion	dff4	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dff3	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) )
2		df-br	⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
3		ssel	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
4		opelxp2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑦 ∈ 𝐵 )
5	3 4	syl6	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ 𝐵 ) )
6	2 5	syl5bi	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 → 𝑦 ∈ 𝐵 ) )
7	6	pm4.71rd	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
8	7	eubidv	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
9		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
10	8 9	bitr4di	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
11	10	ralbidv	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
12	11	pm5.32i	⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
13	1 12	bitri	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )