Theorem ercpbllem

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

	Ref	Expression
Hypotheses	ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
	ercpbllem.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	ercpbllem	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∼ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
2		ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
3		ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4		ercpbllem.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5	1 2 3	divsfval	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )
6	1 2 3	divsfval	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = [ 𝐵 ] ∼ )
7	5 6	eqeq12d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ [ 𝐴 ] ∼ = [ 𝐵 ] ∼ ) )
8	1 4	erth	⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ [ 𝐴 ] ∼ = [ 𝐵 ] ∼ ) )
9	7 8	bitr4d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∼ 𝐵 ) )