Theorem funsneqopb

Description: A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funsndifnop.a	|- A e. _V
	funsndifnop.b	|- B e. _V
	funsndifnop.g	|- G = { <. A , B >. }
Assertion	funsneqopb	|- ( A = B <-> G e. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	|- A e. _V
2		funsndifnop.b	|- B e. _V
3		funsndifnop.g	|- G = { <. A , B >. }
4		opeq1	|- ( A = B -> <. A , B >. = <. B , B >. )
5	4	sneqd	|- ( A = B -> { <. A , B >. } = { <. B , B >. } )
6	2	snopeqopsnid	|- { <. B , B >. } = <. { B } , { B } >.
7	5 6	eqtrdi	|- ( A = B -> { <. A , B >. } = <. { B } , { B } >. )
8	3 7	eqtrid	|- ( A = B -> G = <. { B } , { B } >. )
9		snex	|- { B } e. _V
10	9 9	opelvv	|- <. { B } , { B } >. e. ( _V X. _V )
11	8 10	eqeltrdi	|- ( A = B -> G e. ( _V X. _V ) )
12	1 2 3	funsndifnop	|- ( A =/= B -> -. G e. ( _V X. _V ) )
13	12	necon4ai	|- ( G e. ( _V X. _V ) -> A = B )
14	11 13	impbii	|- ( A = B <-> G e. ( _V X. _V ) )