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	syl6bi	⊢ ( 𝐴 = 𝐶 → ( ¬ 𝐶 ∈ 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	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ) )