Metamath Proof Explorer

Theorem rabbi

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

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

Proof

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