Theorem rabeqsnd

Description: Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021)

	Ref	Expression
Hypotheses	rabeqsnd.0	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	rabeqsnd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	rabeqsnd.2	⊢ ( 𝜑 → 𝜒 )
	rabeqsnd.3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 = 𝐵 )
Assertion	rabeqsnd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		rabeqsnd.0	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2		rabeqsnd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		rabeqsnd.2	⊢ ( 𝜑 → 𝜒 )
4		rabeqsnd.3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 = 𝐵 )
5	4	expl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) )
6	5	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) )
7	2 3	jca	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) )
8	7	a1d	⊢ ( 𝜑 → ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
9	8	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
10		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
11	10 1	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
12	11	pm5.74i	⊢ ( ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
13	12	albii	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
14	9 13	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
15	6 14	jca	⊢ ( 𝜑 → ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) )
16		albiim	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) )
17	15 16	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) )
18		rabeqsn	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) )
19	17 18	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } )