rmob

Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Hypotheses	rmoi.b	$⊢ x = B \to (φ \leftrightarrow ψ)$
	rmoi.c	$⊢ x = C \to (φ \leftrightarrow χ)$
Assertion	rmob	$⊢ (\exists^{*} x \in A φ \land (B \in A \land ψ)) \to (B = C \leftrightarrow (C \in A \land χ))$

Proof

Step	Hyp	Ref	Expression
1		rmoi.b	$⊢ x = B \to (φ \leftrightarrow ψ)$
2		rmoi.c	$⊢ x = C \to (φ \leftrightarrow χ)$
3		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
4		simprl	$⊢ (\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to B \in A$
5		eleq1	$⊢ B = C \to (B \in A \leftrightarrow C \in A)$
6	4 5	syl5ibcom	$⊢ (\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to (B = C \to C \in A)$
7		simpl	$⊢ (C \in A \land χ) \to C \in A$
8	7	a1i	$⊢ (\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to ((C \in A \land χ) \to C \in A)$
9	4	anim1i	$⊢ ((\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \land C \in A) \to (B \in A \land C \in A)$
10		simpll	$⊢ ((\exists^{} x (x \in A \land φ) \land (B \in A \land ψ)) \land C \in A) \to \exists^{} x (x \in A \land φ)$
11		simplr	$⊢ ((\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \land C \in A) \to (B \in A \land ψ)$
12		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
13	12 1	anbi12d	$⊢ x = B \to ((x \in A \land φ) \leftrightarrow (B \in A \land ψ))$
14		eleq1	$⊢ x = C \to (x \in A \leftrightarrow C \in A)$
15	14 2	anbi12d	$⊢ x = C \to ((x \in A \land φ) \leftrightarrow (C \in A \land χ))$
16	13 15	mob	$⊢ ((B \in A \land C \in A) \land \exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to (B = C \leftrightarrow (C \in A \land χ))$
17	9 10 11 16	syl3anc	$⊢ ((\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \land C \in A) \to (B = C \leftrightarrow (C \in A \land χ))$
18	17	ex	$⊢ (\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to (C \in A \to (B = C \leftrightarrow (C \in A \land χ)))$
19	6 8 18	pm5.21ndd	$⊢ (\exists^{*} x (x \in A \land φ) \land (B \in A \land ψ)) \to (B = C \leftrightarrow (C \in A \land χ))$
20	3 19	sylanb	$⊢ (\exists^{*} x \in A φ \land (B \in A \land ψ)) \to (B = C \leftrightarrow (C \in A \land χ))$

Metamath Proof Explorer

Theorem rmob

Proof