Theorem bnj1465

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

	Ref	Expression
Hypotheses	bnj1465.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	bnj1465.2	$$⊢\psi \to \forall x\psi$$
	bnj1465.3	$$⊢\chi \to \psi$$
Assertion	bnj1465	$$⊢\left(\chi \wedge A\in V\right)\to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj1465.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		bnj1465.2	$$⊢\psi \to \forall x\psi$$
3		bnj1465.3	$$⊢\chi \to \psi$$
4	3	adantr	$$⊢\left(\chi \wedge A\in V\right)\to \psi$$
5	2 1	bnj1464	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
6	5	adantl	$$⊢\left(\chi \wedge A\in V\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
7	4 6	mpbird	$$⊢\left(\chi \wedge A\in V\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
8	7	spesbcd	$$⊢\left(\chi \wedge A\in V\right)\to \exists x\phi$$