Theorem disjeq1i

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

	Ref	Expression
Hypothesis	disjeq1i.1	$$⊢A=B$$
Assertion	disjeq1i	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in B}{Disj}C$$

Proof

Step	Hyp	Ref	Expression
1		disjeq1i.1	$$⊢A=B$$
2	1	rmoeqi	$$⊢{\exists }^{*}x\in At\in C\leftrightarrow {\exists }^{*}x\in Bt\in C$$
3	2	albii	$$⊢\forall t{\exists }^{*}x\in At\in C\leftrightarrow \forall t{\exists }^{*}x\in Bt\in C$$
4		df-disj	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall t{\exists }^{*}x\in At\in C$$
5		df-disj	$$⊢\underset{x\in B}{Disj}C\leftrightarrow \forall t{\exists }^{*}x\in Bt\in C$$
6	3 4 5	3bitr4i	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in B}{Disj}C$$