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	|- ( Disj_ x e. A C <-> Disj_ x e. B D )

Proof

Step	Hyp	Ref	Expression
1		disjeq12i.1	|- A = B
2		disjeq12i.2	|- C = D
3		disjeq2	|- ( A. x e. A C = D -> ( Disj_ x e. A C <-> Disj_ x e. A D ) )
4	2	a1i	|- ( x e. A -> C = D )
5	3 4	mprg	|- ( Disj_ x e. A C <-> Disj_ x e. A D )
6	1	disjeq1i	|- ( Disj_ x e. A D <-> Disj_ x e. B D )
7	5 6	bitri	|- ( Disj_ x e. A C <-> Disj_ x e. B D )