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

Metamath Proof Explorer

Theorem exbii

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994)

		Ref	Expression
	Hypothesis	exbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	exbii	$⊢ \exists x φ \leftrightarrow \exists x ψ$

Step	Hyp	Ref	Expression
1		exbii.1	$⊢ φ \leftrightarrow ψ$
2		exbi	$⊢ \forall x (φ \leftrightarrow ψ) \to (\exists x φ \leftrightarrow \exists x ψ)$
3	2 1	mpg	$⊢ \exists x φ \leftrightarrow \exists x ψ$