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 ⊢ φ → A ∈ V
preqsnd.2 ⊢ φ → B ∈ W
Assertion preqsnd ⊢ φ → A B = C ↔ A = C ∧ B = C

Proof

Step Hyp Ref Expression
1 preqsnd.1 ⊢ φ → A ∈ V
2 preqsnd.2 ⊢ φ → B ∈ W
3 1 adantl ⊢ C ∈ V ∧ φ → A ∈ V
4 2 adantl ⊢ C ∈ V ∧ φ → B ∈ W
5 simpl ⊢ C ∈ V ∧ φ → C ∈ V
6 dfsn2 ⊢ C = C C
7 6 eqeq2i ⊢ A B = C ↔ A B = C C
8 preq12bg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ C ∈ 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 ∈ V ∧ B ∈ W ∧ C ∈ V ∧ C ∈ V → A B = C C ↔ A = C ∧ B = C
11 7 10 bitrid ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ C ∈ V → A B = C ↔ A = C ∧ B = C
12 3 4 5 5 11 syl22anc ⊢ C ∈ V ∧ φ → A B = C ↔ A = C ∧ B = C
13 snprc ⊢ ¬ C ∈ V ↔ C = ∅
14 13 biimpi ⊢ ¬ C ∈ V → C = ∅
15 14 adantr ⊢ ¬ C ∈ V ∧ φ → C = ∅
16 15 eqeq2d ⊢ ¬ C ∈ V ∧ φ → A B = C ↔ A B = ∅
17 prnzg ⊢ A ∈ V → A B ≠ ∅
18 eqneqall ⊢ A B = ∅ → A B ≠ ∅ → A = C ∧ B = C
19 17 18 syl5com ⊢ A ∈ V → A B = ∅ → A = C ∧ B = C
20 1 19 syl ⊢ φ → A B = ∅ → A = C ∧ B = C
21 20 adantl ⊢ ¬ C ∈ V ∧ φ → A B = ∅ → A = C ∧ B = C
22 16 21 sylbid ⊢ ¬ C ∈ V ∧ φ → A B = C → A = C ∧ B = C
23 eleq1 ⊢ C = A → C ∈ V ↔ A ∈ V
24 23 eqcoms ⊢ A = C → C ∈ V ↔ A ∈ V
25 24 notbid ⊢ A = C → ¬ C ∈ V ↔ ¬ A ∈ V
26 pm2.24 ⊢ A ∈ V → ¬ A ∈ V → B = C → A B = C
27 elex ⊢ A ∈ V → A ∈ V
28 26 27 syl11 ⊢ ¬ A ∈ V → A ∈ V → B = C → A B = C
29 25 28 biimtrdi ⊢ A = C → ¬ C ∈ V → A ∈ V → B = C → A B = C
30 29 com13 ⊢ A ∈ V → ¬ C ∈ V → A = C → B = C → A B = C
31 1 30 syl ⊢ φ → ¬ C ∈ V → A = C → B = C → A B = C
32 31 impcom ⊢ ¬ C ∈ V ∧ φ → A = C → B = C → A B = C
33 32 impd ⊢ ¬ C ∈ V ∧ φ → A = C ∧ B = C → A B = C
34 22 33 impbid ⊢ ¬ C ∈ V ∧ φ → A B = C ↔ A = C ∧ B = C
35 12 34 pm2.61ian ⊢ φ → A B = C ↔ A = C ∧ B = C