Theorem funop

Description: An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

	Ref	Expression
Hypotheses	funopsn.x	⊢ 𝑋 ∈ V
	funopsn.y	⊢ 𝑌 ∈ V
Assertion	funop	⊢ ( Fun ⟨ 𝑋 , 𝑌 ⟩ ↔ ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	⊢ 𝑋 ∈ V
2		funopsn.y	⊢ 𝑌 ∈ V
3		eqid	⊢ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑋 , 𝑌 ⟩
4	1 2	funopsn	⊢ ( ( Fun ⟨ 𝑋 , 𝑌 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ ) → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
5	3 4	mpan2	⊢ ( Fun ⟨ 𝑋 , 𝑌 ⟩ → ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) )
6		vex	⊢ 𝑎 ∈ V
7	6 6	funsn	⊢ Fun { ⟨ 𝑎 , 𝑎 ⟩ }
8		funeq	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } → ( Fun ⟨ 𝑋 , 𝑌 ⟩ ↔ Fun { ⟨ 𝑎 , 𝑎 ⟩ } ) )
9	7 8	mpbiri	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } → Fun ⟨ 𝑋 , 𝑌 ⟩ )
10	9	adantl	⊢ ( ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) → Fun ⟨ 𝑋 , 𝑌 ⟩ )
11	10	exlimiv	⊢ ( ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) → Fun ⟨ 𝑋 , 𝑌 ⟩ )
12	5 11	impbii	⊢ ( Fun ⟨ 𝑋 , 𝑌 ⟩ ↔ ∃ 𝑎 ( 𝑋 = { 𝑎 } ∧ ⟨ 𝑋 , 𝑌 ⟩ = { ⟨ 𝑎 , 𝑎 ⟩ } ) )