Theorem fveleq

Description: Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008)

	Ref	Expression
Assertion	fveleq	$$⊢A=B\to \left(\left(\phi \to F\left(A\right)\in P\right)\leftrightarrow \left(\phi \to F\left(B\right)\in P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=B\to F\left(A\right)=F\left(B\right)$$
2	1	eleq1d	$$⊢A=B\to \left(F\left(A\right)\in P\leftrightarrow F\left(B\right)\in P\right)$$
3	2	imbi2d	$$⊢A=B\to \left(\left(\phi \to F\left(A\right)\in P\right)\leftrightarrow \left(\phi \to F\left(B\right)\in P\right)\right)$$