Metamath Proof Explorer

Theorem raleqbi1dvOLD

Description: Obsolete version of raleqbi1dv as of 5-May-2023. Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis raleqd.1 ⊢ A = B → φ ↔ ψ
Assertion raleqbi1dvOLD ⊢ A = B → ∀ x ∈ A φ ↔ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 raleqd.1 ⊢ A = B → φ ↔ ψ
2 raleq ⊢ A = B → ∀ x ∈ A φ ↔ ∀ x ∈ B φ
3 1 ralbidv ⊢ A = B → ∀ x ∈ B φ ↔ ∀ x ∈ B ψ
4 2 3 bitrd ⊢ A = B → ∀ x ∈ A φ ↔ ∀ x ∈ B ψ