Metamath Proof Explorer

Theorem rabrabi

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022) Avoid ax-10 , ax-11 and ax-12 . (Revised by GG, 12-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		rabrabi.1	$⊢ x = y \to (χ \leftrightarrow φ)$
2		df-rab	$⊢ \{y \in A \| φ\} = \{y \| (y \in A \land φ)\}$
3	2	eleq2i	$⊢ x \in \{y \in A \| φ\} \leftrightarrow x \in \{y \| (y \in A \land φ)\}$
4		df-clab	$⊢ x \in \{y \| (y \in A \land φ)\} \leftrightarrow [x/ y] (y \in A \land φ)$
5		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
6	1	bicomd	$⊢ x = y \to (φ \leftrightarrow χ)$
7	6	equcoms	$⊢ y = x \to (φ \leftrightarrow χ)$
8	5 7	anbi12d	$⊢ y = x \to ((y \in A \land φ) \leftrightarrow (x \in A \land χ))$
9	8	sbievw	$⊢ [x/ y] (y \in A \land φ) \leftrightarrow (x \in A \land χ)$
10	3 4 9	3bitri	$⊢ x \in \{y \in A \| φ\} \leftrightarrow (x \in A \land χ)$
11	10	anbi1i	$⊢ (x \in \{y \in A \| φ\} \land ψ) \leftrightarrow ((x \in A \land χ) \land ψ)$
12		anass	$⊢ ((x \in A \land χ) \land ψ) \leftrightarrow (x \in A \land (χ \land ψ))$
13	11 12	bitri	$⊢ (x \in \{y \in A \| φ\} \land ψ) \leftrightarrow (x \in A \land (χ \land ψ))$
14	13	rabbia2	$⊢ \{x \in \{y \in A \| φ\} \| ψ\} = \{x \in A \| (χ \land ψ)\}$