Theorem fun2dmnop

Description: A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020) (Proof shortened by AV, 9-Jun-2021)

	Ref	Expression
Hypotheses	fun2dmnop.a	⊢ 𝐴 ∈ V
	fun2dmnop.b	⊢ 𝐵 ∈ V
Assertion	fun2dmnop	⊢ ( ( Fun 𝐺 ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ¬ 𝐺 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		fun2dmnop.a	⊢ 𝐴 ∈ V
2		fun2dmnop.b	⊢ 𝐵 ∈ V
3		fundif	⊢ ( Fun 𝐺 → Fun ( 𝐺 ∖ { ∅ } ) )
4	1 2	fun2dmnop0	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ¬ 𝐺 ∈ ( V × V ) )
5	3 4	syl3an1	⊢ ( ( Fun 𝐺 ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ¬ 𝐺 ∈ ( V × V ) )