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

Metamath Proof Explorer

Theorem eqab2

Description: Implication of a class abstraction. (Contributed by Peter Mazsa, 16-Apr-2019)

		Ref	Expression
	Assertion	eqab2	$⊢ \forall x (x \in A \leftrightarrow φ) \to \forall x \in A φ$

Step	Hyp	Ref	Expression
1		biimp	$⊢ (x \in A \leftrightarrow φ) \to (x \in A \to φ)$
2	1	alimi	$⊢ \forall x (x \in A \leftrightarrow φ) \to \forall x (x \in A \to φ)$
3		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
4	2 3	sylibr	$⊢ \forall x (x \in A \leftrightarrow φ) \to \forall x \in A φ$