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

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 biimpi 
 |-  ( -. C e. _V -> { C } = (/) )
15 14 adantr 
 |-  ( ( -. C e. _V /\ ph ) -> { C } = (/) )
16 15 eqeq2d 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } <-> { A , B } = (/) ) )
17 prnzg 
 |-  ( A e. V -> { A , B } =/= (/) )
18 eqneqall 
 |-  ( { A , B } = (/) -> ( { A , B } =/= (/) -> ( A = C /\ B = C ) ) )
19 17 18 syl5com 
 |-  ( A e. V -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
20 1 19 syl 
 |-  ( ph -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
21 20 adantl 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = (/) -> ( A = C /\ B = C ) ) )
22 16 21 sylbid 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } -> ( A = C /\ B = C ) ) )
23 eleq1 
 |-  ( C = A -> ( C e. _V <-> A e. _V ) )
24 23 eqcoms 
 |-  ( A = C -> ( C e. _V <-> A e. _V ) )
25 24 notbid 
 |-  ( A = C -> ( -. C e. _V <-> -. A e. _V ) )
26 pm2.24 
 |-  ( A e. _V -> ( -. A e. _V -> ( B = C -> { A , B } = { C } ) ) )
27 elex 
 |-  ( A e. V -> A e. _V )
28 26 27 syl11 
 |-  ( -. A e. _V -> ( A e. V -> ( B = C -> { A , B } = { C } ) ) )
29 25 28 biimtrdi 
 |-  ( A = C -> ( -. C e. _V -> ( A e. V -> ( B = C -> { A , B } = { C } ) ) ) )
30 29 com13 
 |-  ( A e. V -> ( -. C e. _V -> ( A = C -> ( B = C -> { A , B } = { C } ) ) ) )
31 1 30 syl 
 |-  ( ph -> ( -. C e. _V -> ( A = C -> ( B = C -> { A , B } = { C } ) ) ) )
32 31 impcom 
 |-  ( ( -. C e. _V /\ ph ) -> ( A = C -> ( B = C -> { A , B } = { C } ) ) )
33 32 impd 
 |-  ( ( -. C e. _V /\ ph ) -> ( ( A = C /\ B = C ) -> { A , B } = { C } ) )
34 22 33 impbid 
 |-  ( ( -. C e. _V /\ ph ) -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
35 12 34 pm2.61ian 
 |-  ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )