reurab

Description: Restricted existential uniqueness of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Hypothesis	reurab.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	reurab	$⊢ \exists! x \in \{y \in A \| ψ\} χ \leftrightarrow \exists! x \in A (φ \land χ)$

Step	Hyp	Ref	Expression
1		reurab.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2	1	bicomd	$⊢ x = y \to (ψ \leftrightarrow φ)$
3	2	equcoms	$⊢ y = x \to (ψ \leftrightarrow φ)$
4	3	elrab	$⊢ x \in \{y \in A \| ψ\} \leftrightarrow (x \in A \land φ)$
5	4	anbi1i	$⊢ (x \in \{y \in A \| ψ\} \land χ) \leftrightarrow ((x \in A \land φ) \land χ)$
6		anass	$⊢ ((x \in A \land φ) \land χ) \leftrightarrow (x \in A \land (φ \land χ))$
7	5 6	bitri	$⊢ (x \in \{y \in A \| ψ\} \land χ) \leftrightarrow (x \in A \land (φ \land χ))$
8	7	eubii	$⊢ \exists! x (x \in \{y \in A \| ψ\} \land χ) \leftrightarrow \exists! x (x \in A \land (φ \land χ))$
9		df-reu	$⊢ \exists! x \in \{y \in A \| ψ\} χ \leftrightarrow \exists! x (x \in \{y \in A \| ψ\} \land χ)$
10		df-reu	$⊢ \exists! x \in A (φ \land χ) \leftrightarrow \exists! x (x \in A \land (φ \land χ))$
11	8 9 10	3bitr4i	$⊢ \exists! x \in \{y \in A \| ψ\} χ \leftrightarrow \exists! x \in A (φ \land χ)$

Metamath Proof Explorer