rabeqsnd

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

Step	Hyp	Ref	Expression
1		rabeqsnd.0	$⊢ x = B \to (ψ \leftrightarrow χ)$
2		rabeqsnd.1	$⊢ φ \to B \in A$
3		rabeqsnd.2	$⊢ φ \to χ$
4		rabeqsnd.3	$⊢ ((φ \land x \in A) \land ψ) \to x = B$
5	4	expl	$⊢ φ \to ((x \in A \land ψ) \to x = B)$
6	5	alrimiv	$⊢ φ \to \forall x ((x \in A \land ψ) \to x = B)$
7	2 3	jca	$⊢ φ \to (B \in A \land χ)$
8	7	a1d	$⊢ φ \to (x = B \to (B \in A \land χ))$
9	8	alrimiv	$⊢ φ \to \forall x (x = B \to (B \in A \land χ))$
10		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
11	10 1	anbi12d	$⊢ x = B \to ((x \in A \land ψ) \leftrightarrow (B \in A \land χ))$
12	11	pm5.74i	$⊢ (x = B \to (x \in A \land ψ)) \leftrightarrow (x = B \to (B \in A \land χ))$
13	12	albii	$⊢ \forall x (x = B \to (x \in A \land ψ)) \leftrightarrow \forall x (x = B \to (B \in A \land χ))$
14	9 13	sylibr	$⊢ φ \to \forall x (x = B \to (x \in A \land ψ))$
15	6 14	jca	$⊢ φ \to (\forall x ((x \in A \land ψ) \to x = B) \land \forall x (x = B \to (x \in A \land ψ)))$
16		albiim	$⊢ \forall x ((x \in A \land ψ) \leftrightarrow x = B) \leftrightarrow (\forall x ((x \in A \land ψ) \to x = B) \land \forall x (x = B \to (x \in A \land ψ)))$
17	15 16	sylibr	$⊢ φ \to \forall x ((x \in A \land ψ) \leftrightarrow x = B)$
18		rabeqsn	$⊢ \{x \in A \| ψ\} = \{B\} \leftrightarrow \forall x ((x \in A \land ψ) \leftrightarrow x = B)$
19	17 18	sylibr	$⊢ φ \to \{x \in A \| ψ\} = \{B\}$

Metamath Proof Explorer