Theorem disjeq1i

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

	Ref	Expression
Hypothesis	disjeq1i.1	⊢ 𝐴 = 𝐵
Assertion	disjeq1i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		disjeq1i.1	⊢ 𝐴 = 𝐵
2	1	rmoeqi	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃* 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 )
3	2	albii	⊢ ( ∀ 𝑡 ∃* 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∀ 𝑡 ∃* 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 )
4		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑡 ∃* 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 )
5		df-disj	⊢ ( Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑡 ∃* 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 )
6	3 4 5	3bitr4i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶 )