Metamath Proof Explorer

Theorem disjeq12dv

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

Ref Expression
Hypotheses disjeq12dv.1 ⊢ φ → A = B
disjeq12dv.2 ⊢ φ → C = D
Assertion disjeq12dv ⊢ φ → Disj x ∈ A C ↔ Disj x ∈ B D

Proof

Step Hyp Ref Expression
1 disjeq12dv.1 ⊢ φ → A = B
2 disjeq12dv.2 ⊢ φ → C = D
3 1 eleq2d ⊢ φ → x ∈ A ↔ x ∈ B
4 3 anbi1d ⊢ φ → x ∈ A ∧ t ∈ C ↔ x ∈ B ∧ t ∈ C
5 4 mobidv ⊢ φ → ∃* x x ∈ A ∧ t ∈ C ↔ ∃* x x ∈ B ∧ t ∈ C
6 df-rmo ⊢ ∃* x ∈ A t ∈ C ↔ ∃* x x ∈ A ∧ t ∈ C
7 df-rmo ⊢ ∃* x ∈ B t ∈ C ↔ ∃* x x ∈ B ∧ t ∈ C
8 5 6 7 3bitr4g ⊢ φ → ∃* x ∈ A t ∈ C ↔ ∃* x ∈ B t ∈ C
9 8 albidv ⊢ φ → ∀ t ∃* x ∈ A t ∈ C ↔ ∀ t ∃* x ∈ B t ∈ C
10 df-disj ⊢ Disj x ∈ A C ↔ ∀ t ∃* x ∈ A t ∈ C
11 df-disj ⊢ Disj x ∈ B C ↔ ∀ t ∃* x ∈ B t ∈ C
12 9 10 11 3bitr4g ⊢ φ → Disj x ∈ A C ↔ Disj x ∈ B C
13 2 adantr ⊢ φ ∧ x ∈ B → C = D
14 13 disjeq2dv ⊢ φ → Disj x ∈ B C ↔ Disj x ∈ B D
15 12 14 bitrd ⊢ φ → Disj x ∈ A C ↔ Disj x ∈ B D