Theorem disjeq12dv

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

	Ref	Expression
Hypotheses	disjeq12dv.1	|- ( ph -> A = B )
	disjeq12dv.2	|- ( ph -> C = D )
Assertion	disjeq12dv	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B D ) )

Proof

Step	Hyp	Ref	Expression
1		disjeq12dv.1	|- ( ph -> A = B )
2		disjeq12dv.2	|- ( ph -> C = D )
3	1	eleq2d	|- ( ph -> ( x e. A <-> x e. B ) )
4	3	anbi1d	|- ( ph -> ( ( x e. A /\ t e. C ) <-> ( x e. B /\ t e. C ) ) )
5	4	mobidv	|- ( ph -> ( E* x ( x e. A /\ t e. C ) <-> E* x ( x e. B /\ t e. C ) ) )
6		df-rmo	|- ( E* x e. A t e. C <-> E* x ( x e. A /\ t e. C ) )
7		df-rmo	|- ( E* x e. B t e. C <-> E* x ( x e. B /\ t e. C ) )
8	5 6 7	3bitr4g	|- ( ph -> ( E* x e. A t e. C <-> E* x e. B t e. C ) )
9	8	albidv	|- ( ph -> ( A. t E* x e. A t e. C <-> A. t E* x e. B t e. C ) )
10		df-disj	|- ( Disj_ x e. A C <-> A. t E* x e. A t e. C )
11		df-disj	|- ( Disj_ x e. B C <-> A. t E* x e. B t e. C )
12	9 10 11	3bitr4g	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )
13	2	adantr	|- ( ( ph /\ x e. B ) -> C = D )
14	13	disjeq2dv	|- ( ph -> ( Disj_ x e. B C <-> Disj_ x e. B D ) )
15	12 14	bitrd	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B D ) )