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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
preqsnd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion preqsnd ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 preqsnd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 preqsnd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 1 adantl ⊢ ( ( 𝐶 ∈ V ∧ 𝜑 ) → 𝐴 ∈ 𝑉 )
4 2 adantl ⊢ ( ( 𝐶 ∈ V ∧ 𝜑 ) → 𝐵 ∈ 𝑊 )
5 simpl ⊢ ( ( 𝐶 ∈ V ∧ 𝜑 ) → 𝐶 ∈ V )
6 dfsn2 ⊢ { 𝐶 } = { 𝐶 , 𝐶 }
7 6 eqeq2i ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐶 } )
8 preq12bg ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐶 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) ) )
9 oridm ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) )
10 8 9 bitrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
11 7 10 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
12 3 4 5 5 11 syl22anc ⊢ ( ( 𝐶 ∈ V ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
13 snprc ⊢ ( ¬ 𝐶 ∈ V ↔ { 𝐶 } = ∅ )
14 13 biimpi ⊢ ( ¬ 𝐶 ∈ V → { 𝐶 } = ∅ )
15 14 adantr ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → { 𝐶 } = ∅ )
16 15 eqeq2d ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ { 𝐴 , 𝐵 } = ∅ ) )
17 prnzg ⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 , 𝐵 } ≠ ∅ )
18 eqneqall ⊢ ( { 𝐴 , 𝐵 } = ∅ → ( { 𝐴 , 𝐵 } ≠ ∅ → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
19 17 18 syl5com ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 , 𝐵 } = ∅ → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
20 1 19 syl ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } = ∅ → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
21 20 adantl ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = ∅ → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
22 16 21 sylbid ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝐶 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
23 eleq1 ⊢ ( 𝐶 = 𝐴 → ( 𝐶 ∈ V ↔ 𝐴 ∈ V ) )
24 23 eqcoms ⊢ ( 𝐴 = 𝐶 → ( 𝐶 ∈ V ↔ 𝐴 ∈ V ) )
25 24 notbid ⊢ ( 𝐴 = 𝐶 → ( ¬ 𝐶 ∈ V ↔ ¬ 𝐴 ∈ V ) )
26 pm2.24 ⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ V → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) )
27 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
28 26 27 syl11 ⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 ∈ 𝑉 → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) )
29 25 28 biimtrdi ⊢ ( 𝐴 = 𝐶 → ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ 𝑉 → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) ) )
30 29 com13 ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐶 ∈ V → ( 𝐴 = 𝐶 → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) ) )
31 1 30 syl ⊢ ( 𝜑 → ( ¬ 𝐶 ∈ V → ( 𝐴 = 𝐶 → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) ) )
32 31 impcom ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( 𝐴 = 𝐶 → ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 } ) ) )
33 32 impd ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 } ) )
34 22 33 impbid ⊢ ( ( ¬ 𝐶 ∈ V ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )
35 12 34 pm2.61ian ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )