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 birani ⊢ ¬ C ∈ V ∧ φ → C = ∅
15 14 eqeq2d ⊢ ¬ C ∈ V ∧ φ → A B = C ↔ A B = ∅
16 prnzg ⊢ A ∈ V → A B ≠ ∅
17 eqneqall ⊢ A B = ∅ → A B ≠ ∅ → A = C ∧ B = C
18 16 17 syl5com ⊢ A ∈ V → A B = ∅ → A = C ∧ B = C
19 1 18 syl ⊢ φ → A B = ∅ → A = C ∧ B = C
20 19 adantl ⊢ ¬ C ∈ V ∧ φ → A B = ∅ → A = C ∧ B = C
21 15 20 sylbid ⊢ ¬ C ∈ V ∧ φ → A B = C → A = C ∧ B = C
22 eleq1 ⊢ C = A → C ∈ V ↔ A ∈ V
23 22 eqcoms ⊢ A = C → C ∈ V ↔ A ∈ V
24 23 notbid ⊢ A = C → ¬ C ∈ V ↔ ¬ A ∈ V
25 pm2.24 ⊢ A ∈ V → ¬ A ∈ V → B = C → A B = C
26 elex ⊢ A ∈ V → A ∈ V
27 25 26 syl11 ⊢ ¬ A ∈ V → A ∈ V → B = C → A B = C
28 24 27 biimtrdi ⊢ A = C → ¬ C ∈ V → A ∈ V → B = C → A B = C
29 28 com13 ⊢ A ∈ V → ¬ C ∈ V → A = C → B = C → A B = C
30 1 29 syl ⊢ φ → ¬ C ∈ V → A = C → B = C → A B = C
31 30 impcom ⊢ ¬ C ∈ V ∧ φ → A = C → B = C → A B = C
32 31 impd ⊢ ¬ C ∈ V ∧ φ → A = C ∧ B = C → A B = C
33 21 32 impbid ⊢ ¬ C ∈ V ∧ φ → A B = C ↔ A = C ∧ B = C
34 12 33 pm2.61ian ⊢ φ → A B = C ↔ A = C ∧ B = C