Theorem disjeq12i

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

	Ref	Expression
Hypotheses	disjeq12i.1	$$⊢A=B$$
	disjeq12i.2	$$⊢C=D$$
Assertion	disjeq12i	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in B}{Disj}D$$

Proof

Step	Hyp	Ref	Expression
1		disjeq12i.1	$$⊢A=B$$
2		disjeq12i.2	$$⊢C=D$$
3		disjeq2	$$⊢\forall x\in AC=D\to \left(\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in A}{Disj}D\right)$$
4	2	a1i	$$⊢x\in A\to C=D$$
5	3 4	mprg	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in A}{Disj}D$$
6	1	disjeq1i	$$⊢\underset{x\in A}{Disj}D\leftrightarrow \underset{x\in B}{Disj}D$$
7	5 6	bitri	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \underset{x\in B}{Disj}D$$