This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )