Theorem ercpbllem

Description: Lemma for ercpbl . (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	ercpbl.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
	ercpbl.v	$$⊢\phi \to V\in W$$
	ercpbl.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
	ercpbllem.1	$$⊢\phi \to A\in V$$
Assertion	ercpbllem	$$⊢\phi \to \left(F\left(A\right)=F\left(B\right)\leftrightarrow A\underset{\dot{}}{\sim }B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
2		ercpbl.v	$$⊢\phi \to V\in W$$
3		ercpbl.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
4		ercpbllem.1	$$⊢\phi \to A\in V$$
5	1 2 3	divsfval	$$⊢\phi \to F\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$
6	1 2 3	divsfval	$$⊢\phi \to F\left(B\right)=\left[B\right]\underset{\dot{}}{\sim }$$
7	5 6	eqeq12d	$$⊢\phi \to \left(F\left(A\right)=F\left(B\right)\leftrightarrow \left[A\right]\underset{\dot{}}{\sim }=\left[B\right]\underset{\dot{}}{\sim }\right)$$
8	1 4	erth	$$⊢\phi \to \left(A\underset{\dot{}}{\sim }B\leftrightarrow \left[A\right]\underset{\dot{}}{\sim }=\left[B\right]\underset{\dot{}}{\sim }\right)$$
9	7 8	bitr4d	$$⊢\phi \to \left(F\left(A\right)=F\left(B\right)\leftrightarrow A\underset{\dot{}}{\sim }B\right)$$