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	2	ralrid	$⊢ \forall x (x \in A \leftrightarrow φ) \to \forall x \in A φ$