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	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	eqelbid.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
Assertion	eqelbid	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eqelbid.1	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
2		eqelbid.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
3		eqeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐵 ↔ 𝐵 = 𝐵 ) )
4		eqeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐶 ↔ 𝐵 = 𝐶 ) )
5	3 4	bibi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) ) )
6		eqid	⊢ 𝐵 = 𝐵
7	6	tbt	⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 = 𝐶 ↔ 𝐵 = 𝐵 ) )
8		bicom	⊢ ( ( 𝐵 = 𝐶 ↔ 𝐵 = 𝐵 ) ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) )
9	7 8	bitri	⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 = 𝐵 ↔ 𝐵 = 𝐶 ) )
10	5 9	bitr4di	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )
11		simpr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
12	1	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → 𝐵 ∈ 𝐴 )
13	10 11 12	rspcdva	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ) → 𝐵 = 𝐶 )
14		simplr	⊢ ( ( ( 𝜑 ∧ 𝐵 = 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
15	14	eqeq2d	⊢ ( ( ( 𝜑 ∧ 𝐵 = 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
16	15	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) )
17	13 16	impbida	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 ↔ 𝑥 = 𝐶 ) ↔ 𝐵 = 𝐶 ) )