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

Metamath Proof Explorer

Theorem bnj1521

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1521.1	$⊢ χ \to \exists x \in B φ$
	bnj1521.2	$⊢ θ \leftrightarrow (χ \land x \in B \land φ)$
	bnj1521.3	$⊢ χ \to \forall x χ$
Assertion	bnj1521	$⊢ χ \to \exists x θ$

Step	Hyp	Ref	Expression
1		bnj1521.1	$⊢ χ \to \exists x \in B φ$
2		bnj1521.2	$⊢ θ \leftrightarrow (χ \land x \in B \land φ)$
3		bnj1521.3	$⊢ χ \to \forall x χ$
4	1	bnj1196	$⊢ χ \to \exists x (x \in B \land φ)$
5	4 2 3	bnj1345	$⊢ χ \to \exists x θ$