rmob2

Description: Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019)

Step	Hyp	Ref	Expression
1		rmoi2.1	$⊢ x = B \to (ψ \leftrightarrow χ)$
2		rmoi2.2	$⊢ φ \to B \in A$
3		rmoi2.3	$⊢ φ \to \exists^{*} x \in A ψ$
4		rmoi2.4	$⊢ φ \to x \in A$
5		rmoi2.5	$⊢ φ \to ψ$
6		df-rmo	$⊢ \exists^{} x \in A ψ \leftrightarrow \exists^{} x (x \in A \land ψ)$
7	3 6	sylib	$⊢ φ \to \exists^{*} x (x \in A \land ψ)$
8		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
9	8 1	anbi12d	$⊢ x = B \to ((x \in A \land ψ) \leftrightarrow (B \in A \land χ))$
10	9	mob2	$⊢ (B \in A \land \exists^{*} x (x \in A \land ψ) \land (x \in A \land ψ)) \to (x = B \leftrightarrow (B \in A \land χ))$
11	2 7 4 5 10	syl112anc	$⊢ φ \to (x = B \leftrightarrow (B \in A \land χ))$
12	2 11	mpbirand	$⊢ φ \to (x = B \leftrightarrow χ)$

Metamath Proof Explorer