Theorem fgraphxp

Description: Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	fgraphxp	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		fgraphopab	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) } )
2		vex	⊢ 𝑎 ∈ V
3		vex	⊢ 𝑏 ∈ V
4	2 3	op1std	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑥 ) = 𝑎 )
5	4	fveq2d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑎 ) )
6	2 3	op2ndd	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑏 )
7	5 6	eqeq12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) )
8	7	rabxp	⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) }
9		df-3an	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) )
10	9	opabbii	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) }
11	8 10	eqtri	⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) }
12	1 11	eqtr4di	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ 𝑥 ) } )