Theorem eqelbid

Description: A variable elimination law for equality within a given set A . See equvel . (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	eqelbid.1	|- ( ph -> B e. A )
	eqelbid.2	|- ( ph -> C e. A )
Assertion	eqelbid	|- ( ph -> ( A. x e. A ( x = B <-> x = C ) <-> B = C ) )

Proof

Step	Hyp	Ref	Expression
1		eqelbid.1	|- ( ph -> B e. A )
2		eqelbid.2	|- ( ph -> C e. A )
3		eqeq1	|- ( x = B -> ( x = B <-> B = B ) )
4		eqeq1	|- ( x = B -> ( x = C <-> B = C ) )
5	3 4	bibi12d	|- ( x = B -> ( ( x = B <-> x = C ) <-> ( B = B <-> B = C ) ) )
6		eqid	|- B = B
7	6	tbt	|- ( B = C <-> ( B = C <-> B = B ) )
8		bicom	|- ( ( B = C <-> B = B ) <-> ( B = B <-> B = C ) )
9	7 8	bitri	|- ( B = C <-> ( B = B <-> B = C ) )
10	5 9	bitr4di	|- ( x = B -> ( ( x = B <-> x = C ) <-> B = C ) )
11		simpr	|- ( ( ph /\ A. x e. A ( x = B <-> x = C ) ) -> A. x e. A ( x = B <-> x = C ) )
12	1	adantr	|- ( ( ph /\ A. x e. A ( x = B <-> x = C ) ) -> B e. A )
13	10 11 12	rspcdva	|- ( ( ph /\ A. x e. A ( x = B <-> x = C ) ) -> B = C )
14		simplr	|- ( ( ( ph /\ B = C ) /\ x e. A ) -> B = C )
15	14	eqeq2d	|- ( ( ( ph /\ B = C ) /\ x e. A ) -> ( x = B <-> x = C ) )
16	15	ralrimiva	|- ( ( ph /\ B = C ) -> A. x e. A ( x = B <-> x = C ) )
17	13 16	impbida	|- ( ph -> ( A. x e. A ( x = B <-> x = C ) <-> B = C ) )