This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabidim1

Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Assertion	rabidim1	$⊢ x \in \{x \in A \| φ\} \to x \in A$

Step	Hyp	Ref	Expression
1		rabid	$⊢ x \in \{x \in A \| φ\} \leftrightarrow (x \in A \land φ)$
2	1	simplbi	$⊢ x \in \{x \in A \| φ\} \to x \in A$