rabid2im

Description: One direction of rabid2 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025)

		Ref	Expression
	Assertion	rabid2im	$⊢ \forall x \in A φ \to A = \{x \in A \| φ\}$

Step	Hyp	Ref	Expression
1		pm4.71	$⊢ (x \in A \to φ) \leftrightarrow (x \in A \leftrightarrow (x \in A \land φ))$
2	1	albii	$⊢ \forall x (x \in A \to φ) \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land φ))$
3		eqab	$⊢ \forall x (x \in A \leftrightarrow (x \in A \land φ)) \to A = \{x \| (x \in A \land φ)\}$
4	2 3	sylbi	$⊢ \forall x (x \in A \to φ) \to A = \{x \| (x \in A \land φ)\}$
5		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
6		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
7	6	eqeq2i	$⊢ A = \{x \in A \| φ\} \leftrightarrow A = \{x \| (x \in A \land φ)\}$
8	4 5 7	3imtr4i	$⊢ \forall x \in A φ \to A = \{x \in A \| φ\}$

Metamath Proof Explorer