Metamath Proof Explorer

Theorem raleqbidvvOLD

Description: Version of raleqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by BJ, 22-Sep-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses raleqbidvv.1 ⊢ φ → A = B
raleqbidvv.2 ⊢ φ → ψ ↔ χ
Assertion raleqbidvvOLD ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B χ

Proof

Step Hyp Ref Expression
1 raleqbidvv.1 ⊢ φ → A = B
2 raleqbidvv.2 ⊢ φ → ψ ↔ χ
3 2 alrimiv ⊢ φ → ∀ x ψ ↔ χ
4 dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B
5 1 4 sylib ⊢ φ → ∀ x x ∈ A ↔ x ∈ B
6 19.26 ⊢ ∀ x ψ ↔ χ ∧ x ∈ A ↔ x ∈ B ↔ ∀ x ψ ↔ χ ∧ ∀ x x ∈ A ↔ x ∈ B
7 3 5 6 sylanbrc ⊢ φ → ∀ x ψ ↔ χ ∧ x ∈ A ↔ x ∈ B
8 imbi12 ⊢ x ∈ A ↔ x ∈ B → ψ ↔ χ → x ∈ A → ψ ↔ x ∈ B → χ
9 8 impcom ⊢ ψ ↔ χ ∧ x ∈ A ↔ x ∈ B → x ∈ A → ψ ↔ x ∈ B → χ
10 7 9 sylg ⊢ φ → ∀ x x ∈ A → ψ ↔ x ∈ B → χ
11 albi ⊢ ∀ x x ∈ A → ψ ↔ x ∈ B → χ → ∀ x x ∈ A → ψ ↔ ∀ x x ∈ B → χ
12 10 11 syl ⊢ φ → ∀ x x ∈ A → ψ ↔ ∀ x x ∈ B → χ
13 df-ral ⊢ ∀ x ∈ A ψ ↔ ∀ x x ∈ A → ψ
14 df-ral ⊢ ∀ x ∈ B χ ↔ ∀ x x ∈ B → χ
15 12 13 14 3bitr4g ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B χ