Theorem ercpbllem

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

	Ref	Expression
Hypotheses	ercpbl.r	|- ( ph -> .~ Er V )
	ercpbl.v	|- ( ph -> V e. W )
	ercpbl.f	|- F = ( x e. V |-> [ x ] .~ )
	ercpbllem.1	|- ( ph -> A e. V )
Assertion	ercpbllem	|- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	|- ( ph -> .~ Er V )
2		ercpbl.v	|- ( ph -> V e. W )
3		ercpbl.f	|- F = ( x e. V |-> [ x ] .~ )
4		ercpbllem.1	|- ( ph -> A e. V )
5	1 2 3	divsfval	|- ( ph -> ( F ` A ) = [ A ] .~ )
6	1 2 3	divsfval	|- ( ph -> ( F ` B ) = [ B ] .~ )
7	5 6	eqeq12d	|- ( ph -> ( ( F ` A ) = ( F ` B ) <-> [ A ] .~ = [ B ] .~ ) )
8	1 4	erth	|- ( ph -> ( A .~ B <-> [ A ] .~ = [ B ] .~ ) )
9	7 8	bitr4d	|- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )