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	|- A e. _V
	fun2dmnop.b	|- B e. _V
Assertion	fun2dmnop	|- ( ( Fun G /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		fun2dmnop.a	|- A e. _V
2		fun2dmnop.b	|- B e. _V
3		fundif	|- ( Fun G -> Fun ( G \ { (/) } ) )
4	1 2	fun2dmnop0	|- ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )
5	3 4	syl3an1	|- ( ( Fun G /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )