Theorem rexbidvALT

Description: Alternate proof of rexbidv , shorter but requires more axioms. (Contributed by NM, 20-Nov-1994) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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