Theorem disjeq12i

Description: Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	disjeq12i.1	⊢ 𝐴 = 𝐵
	disjeq12i.2	⊢ 𝐶 = 𝐷
Assertion	disjeq12i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		disjeq12i.1	⊢ 𝐴 = 𝐵
2		disjeq12i.2	⊢ 𝐶 = 𝐷
3		disjeq2	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 → ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐷 ) )
4	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 = 𝐷 )
5	3 4	mprg	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐷 )
6	1	disjeq1i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐷 ↔ Disj 𝑥 ∈ 𝐵 𝐷 )
7	5 6	bitri	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷 )