Theorem snopeqop

Description: Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	snopeqop.a	|- A e. _V
	snopeqop.b	|- B e. _V
Assertion	snopeqop	|- ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) )

Proof

Step	Hyp	Ref	Expression
1		snopeqop.a	|- A e. _V
2		snopeqop.b	|- B e. _V
3		eqcom	|- ( { <. A , B >. } = <. C , D >. <-> <. C , D >. = { <. A , B >. } )
4		opeqsng	|- ( ( C e. _V /\ D e. _V ) -> ( <. C , D >. = { <. A , B >. } <-> ( C = D /\ <. A , B >. = { C } ) ) )
5	4	ancoms	|- ( ( D e. _V /\ C e. _V ) -> ( <. C , D >. = { <. A , B >. } <-> ( C = D /\ <. A , B >. = { C } ) ) )
6	3 5	bitrid	|- ( ( D e. _V /\ C e. _V ) -> ( { <. A , B >. } = <. C , D >. <-> ( C = D /\ <. A , B >. = { C } ) ) )
7	1 2	opeqsn	|- ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) )
8	7	a1i	|- ( ( D e. _V /\ C e. _V ) -> ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) ) )
9	8	anbi2d	|- ( ( D e. _V /\ C e. _V ) -> ( ( C = D /\ <. A , B >. = { C } ) <-> ( C = D /\ ( A = B /\ C = { A } ) ) ) )
10		3anan12	|- ( ( A = B /\ C = D /\ C = { A } ) <-> ( C = D /\ ( A = B /\ C = { A } ) ) )
11	10	bicomi	|- ( ( C = D /\ ( A = B /\ C = { A } ) ) <-> ( A = B /\ C = D /\ C = { A } ) )
12	11	a1i	|- ( ( D e. _V /\ C e. _V ) -> ( ( C = D /\ ( A = B /\ C = { A } ) ) <-> ( A = B /\ C = D /\ C = { A } ) ) )
13	6 9 12	3bitrd	|- ( ( D e. _V /\ C e. _V ) -> ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) ) )
14		opprc2	|- ( -. D e. _V -> <. C , D >. = (/) )
15	14	eqeq2d	|- ( -. D e. _V -> ( { <. A , B >. } = <. C , D >. <-> { <. A , B >. } = (/) ) )
16		opex	|- <. A , B >. e. _V
17	16	snnz	|- { <. A , B >. } =/= (/)
18		eqneqall	|- ( { <. A , B >. } = (/) -> ( { <. A , B >. } =/= (/) -> ( A = B /\ C = D /\ C = { A } ) ) )
19	17 18	mpi	|- ( { <. A , B >. } = (/) -> ( A = B /\ C = D /\ C = { A } ) )
20	15 19	biimtrdi	|- ( -. D e. _V -> ( { <. A , B >. } = <. C , D >. -> ( A = B /\ C = D /\ C = { A } ) ) )
21	20	adantr	|- ( ( -. D e. _V /\ C e. _V ) -> ( { <. A , B >. } = <. C , D >. -> ( A = B /\ C = D /\ C = { A } ) ) )
22		eleq1	|- ( D = C -> ( D e. _V <-> C e. _V ) )
23	22	notbid	|- ( D = C -> ( -. D e. _V <-> -. C e. _V ) )
24	23	eqcoms	|- ( C = D -> ( -. D e. _V <-> -. C e. _V ) )
25		pm2.21	|- ( -. C e. _V -> ( C e. _V -> { <. A , B >. } = <. C , D >. ) )
26	24 25	biimtrdi	|- ( C = D -> ( -. D e. _V -> ( C e. _V -> { <. A , B >. } = <. C , D >. ) ) )
27	26	impd	|- ( C = D -> ( ( -. D e. _V /\ C e. _V ) -> { <. A , B >. } = <. C , D >. ) )
28	27	3ad2ant2	|- ( ( A = B /\ C = D /\ C = { A } ) -> ( ( -. D e. _V /\ C e. _V ) -> { <. A , B >. } = <. C , D >. ) )
29	28	com12	|- ( ( -. D e. _V /\ C e. _V ) -> ( ( A = B /\ C = D /\ C = { A } ) -> { <. A , B >. } = <. C , D >. ) )
30	21 29	impbid	|- ( ( -. D e. _V /\ C e. _V ) -> ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) ) )
31	13 30	pm2.61ian	|- ( C e. _V -> ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) ) )
32		opprc1	|- ( -. C e. _V -> <. C , D >. = (/) )
33	32	eqeq2d	|- ( -. C e. _V -> ( { <. A , B >. } = <. C , D >. <-> { <. A , B >. } = (/) ) )
34	33 19	biimtrdi	|- ( -. C e. _V -> ( { <. A , B >. } = <. C , D >. -> ( A = B /\ C = D /\ C = { A } ) ) )
35		eleq1	|- ( C = { A } -> ( C e. _V <-> { A } e. _V ) )
36	35	notbid	|- ( C = { A } -> ( -. C e. _V <-> -. { A } e. _V ) )
37		snex	|- { A } e. _V
38	37	pm2.24i	|- ( -. { A } e. _V -> { <. A , B >. } = <. C , D >. )
39	36 38	biimtrdi	|- ( C = { A } -> ( -. C e. _V -> { <. A , B >. } = <. C , D >. ) )
40	39	3ad2ant3	|- ( ( A = B /\ C = D /\ C = { A } ) -> ( -. C e. _V -> { <. A , B >. } = <. C , D >. ) )
41	40	com12	|- ( -. C e. _V -> ( ( A = B /\ C = D /\ C = { A } ) -> { <. A , B >. } = <. C , D >. ) )
42	34 41	impbid	|- ( -. C e. _V -> ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) ) )
43	31 42	pm2.61i	|- ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) )