inab

Description: Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	inab	$⊢ \{x \| φ\} \cap \{x \| ψ\} = \{x \| (φ \land ψ)\}$

Step	Hyp	Ref	Expression
1		sban	$⊢ [y/ x] (φ \land ψ) \leftrightarrow ([y/ x] φ \land [y/ x] ψ)$
2		df-clab	$⊢ y \in \{x \| (φ \land ψ)\} \leftrightarrow [y/ x] (φ \land ψ)$
3		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
4		df-clab	$⊢ y \in \{x \| ψ\} \leftrightarrow [y/ x] ψ$
5	3 4	anbi12i	$⊢ (y \in \{x \| φ\} \land y \in \{x \| ψ\}) \leftrightarrow ([y/ x] φ \land [y/ x] ψ)$
6	1 2 5	3bitr4ri	$⊢ (y \in \{x \| φ\} \land y \in \{x \| ψ\}) \leftrightarrow y \in \{x \| (φ \land ψ)\}$
7	6	ineqri	$⊢ \{x \| φ\} \cap \{x \| ψ\} = \{x \| (φ \land ψ)\}$

Metamath Proof Explorer