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↔∀xx∈A↔x∈B
5 1 4 sylib ⊢φ→∀xx∈A↔x∈B
6 19.26 ⊢∀xψ↔χ∧x∈A↔x∈B↔∀xψ↔χ∧∀xx∈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 ⊢φ→∀xx∈A→ψ↔x∈B→χ
11 albi ⊢∀xx∈A→ψ↔x∈B→χ→∀xx∈A→ψ↔∀xx∈B→χ
12 10 11 syl ⊢φ→∀xx∈A→ψ↔∀xx∈B→χ
13 df-ral ⊢∀x∈Aψ↔∀xx∈A→ψ
14 df-ral ⊢∀x∈Bχ↔∀xx∈B→χ
15 12 13 14 3bitr4g ⊢φ→∀x∈Aψ↔∀x∈Bχ