rabbi

Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii . (Contributed by NM, 25-Nov-2013)

		Ref	Expression
	Assertion	rabbi	$⊢ \forall x \in A (ψ \leftrightarrow χ) \leftrightarrow \{x \in A \| ψ\} = \{x \in A \| χ\}$

Step	Hyp	Ref	Expression
1		abbib	$⊢ \{x \| (x \in A \land ψ)\} = \{x \| (x \in A \land χ)\} \leftrightarrow \forall x ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
2		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
3		df-rab	$⊢ \{x \in A \| χ\} = \{x \| (x \in A \land χ)\}$
4	2 3	eqeq12i	$⊢ \{x \in A \| ψ\} = \{x \in A \| χ\} \leftrightarrow \{x \| (x \in A \land ψ)\} = \{x \| (x \in A \land χ)\}$
5		df-ral	$⊢ \forall x \in A (ψ \leftrightarrow χ) \leftrightarrow \forall x (x \in A \to (ψ \leftrightarrow χ))$
6		pm5.32	$⊢ (x \in A \to (ψ \leftrightarrow χ)) \leftrightarrow ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
7	6	albii	$⊢ \forall x (x \in A \to (ψ \leftrightarrow χ)) \leftrightarrow \forall x ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
8	5 7	bitri	$⊢ \forall x \in A (ψ \leftrightarrow χ) \leftrightarrow \forall x ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
9	1 4 8	3bitr4ri	$⊢ \forall x \in A (ψ \leftrightarrow χ) \leftrightarrow \{x \in A \| ψ\} = \{x \in A \| χ\}$

Metamath Proof Explorer