Metamath Proof Explorer

Theorem preqsnd

Description: Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016) (Revised by AV, 13-Jun-2022) (Revised by AV, 16-Aug-2024)

Ref Expression
Hypotheses preqsnd.1 
|- ( ph -> A e. V )
preqsnd.2 
|- ( ph -> B e. W )
Assertion preqsnd 
|- ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )

Proof

Step Hyp Ref Expression
1 preqsnd.1 
 |-  ( ph -> A e. V )
2 preqsnd.2 
 |-  ( ph -> B e. W )
3 1 adantl 
 |-  ( ( C e. _V /\ ph ) -> A e. V )
4 2 adantl 
 |-  ( ( C e. _V /\ ph ) -> B e. W )
5 simpl 
 |-  ( ( C e. _V /\ ph ) -> C e. _V )
6 dfsn2 
 |-  { C } = { C , C }
7 6 eqeq2i 
 |-  ( { A , B } = { C } <-> { A , B } = { C , C } )
8 preq12bg 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ C e. _V ) ) -> ( { A , B } = { C , C } <-> ( ( A = C /\ B = C ) \/ ( A = C /\ B = C ) ) ) )
9 oridm 
 |-  ( ( ( A = C /\ B = C ) \/ ( A = C /\ B = C ) ) <-> ( A = C /\ B = C ) )
10 8 9 bitrdi 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ C e. _V ) ) -> ( { A , B } = { C , C } <-> ( A = C /\ B = C ) ) )
11 7 10 bitrid 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ C e. _V ) ) -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
12 3 4 5 5 11 syl22anc 
 |-  ( ( C e. _V /\ ph ) -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
13 snprc 
 |-  ( -. C e. _V <-> { C } = (/) )
14 13 birani 
 |-  ( ( -. C e. _V /\ ph ) -> { C } = (/) )
15 14 eqeq2d 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } <-> { A , B } = (/) ) )
16 prnzg 
 |-  ( A e. V -> { A , B } =/= (/) )
17 eqneqall 
 |-  ( { A , B } = (/) -> ( { A , B } =/= (/) -> ( A = C /\ B = C ) ) )
18 16 17 syl5com 
 |-  ( A e. V -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
19 1 18 syl 
 |-  ( ph -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
20 19 adantl 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
21 15 20 sylbid 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } -> ( A = C /\ B = C ) ) )
22 eleq1 
 |-  ( C = A -> ( C e. _V <-> A e. _V ) )
23 22 eqcoms 
 |-  ( A = C -> ( C e. _V <-> A e. _V ) )
24 23 notbid 
 |-  ( A = C -> ( -. C e. _V <-> -. A e. _V ) )
25 pm2.24 
 |-  ( A e. _V -> ( -. A e. _V -> ( B = C -> { A , B } = { C } ) ) )
26 elex 
 |-  ( A e. V -> A e. _V )
27 25 26 syl11 
 |-  ( -. A e. _V -> ( A e. V -> ( B = C -> { A , B } = { C } ) ) )
28 24 27 biimtrdi 
 |-  ( A = C -> ( -. C e. _V -> ( A e. V -> ( B = C -> { A , B } = { C } ) ) ) )
29 28 com13 
 |-  ( A e. V -> ( -. C e. _V -> ( A = C -> ( B = C -> { A , B } = { C } ) ) ) )
30 1 29 syl 
 |-  ( ph -> ( -. C e. _V -> ( A = C -> ( B = C -> { A , B } = { C } ) ) ) )
31 30 impcom 
 |-  ( ( -. C e. _V /\ ph ) -> ( A = C -> ( B = C -> { A , B } = { C } ) ) )
32 31 impd 
 |-  ( ( -. C e. _V /\ ph ) -> ( ( A = C /\ B = C ) -> { A , B } = { C } ) )
33 21 32 impbid 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
34 12 33 pm2.61ian 
 |-  ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )