Theorem bnj1209

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

	Ref	Expression
Hypotheses	bnj1209.1	$$⊢\chi \to \exists x\in B\phi$$
	bnj1209.2	$$⊢\theta \leftrightarrow \left(\chi \wedge x\in B\wedge \phi \right)$$
Assertion	bnj1209	$$⊢\chi \to \exists x\theta$$

Proof

Step	Hyp	Ref	Expression
1		bnj1209.1	$$⊢\chi \to \exists x\in B\phi$$
2		bnj1209.2	$$⊢\theta \leftrightarrow \left(\chi \wedge x\in B\wedge \phi \right)$$
3	1	bnj1196	$$⊢\chi \to \exists x\left(x\in B\wedge \phi \right)$$
4	3	ancli	$$⊢\chi \to \left(\chi \wedge \exists x\left(x\in B\wedge \phi \right)\right)$$
5		19.42v	$$⊢\exists x\left(\chi \wedge \left(x\in B\wedge \phi \right)\right)\leftrightarrow \left(\chi \wedge \exists x\left(x\in B\wedge \phi \right)\right)$$
6	4 5	sylibr	$$⊢\chi \to \exists x\left(\chi \wedge \left(x\in B\wedge \phi \right)\right)$$
7		3anass	$$⊢\left(\chi \wedge x\in B\wedge \phi \right)\leftrightarrow \left(\chi \wedge \left(x\in B\wedge \phi \right)\right)$$
8	2 7	bitri	$$⊢\theta \leftrightarrow \left(\chi \wedge \left(x\in B\wedge \phi \right)\right)$$
9	6 8	bnj1198	$$⊢\chi \to \exists x\theta$$