Theorem rexbidvaALT

Description: Alternate proof of rexbidva , shorter but requires more axioms. (Contributed by NM, 9-Mar-1997) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	rexbidvaALT.1	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	rexbidvaALT	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists x\in A\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexbidvaALT.1	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		nfv	$$⊢Ⅎx\phi$$
3	2 1	rexbida	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists x\in A\chi \right)$$