This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabeqd

Description: Deduction form of rabeq . Note that contrary to rabeq it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019)

Ref Expression
Hypotheses rabeqd.nf ⊢ Ⅎ x φ
rabeqd.1 ⊢ φ → A = B
Assertion rabeqd ⊢ φ → x ∈ A | ψ = x ∈ B | ψ

Proof

Step Hyp Ref Expression
1 rabeqd.nf ⊢ Ⅎ x φ
2 rabeqd.1 ⊢ φ → A = B
3 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
4 3 anbi1d ⊢ A = B → x ∈ A ∧ ψ ↔ x ∈ B ∧ ψ
5 2 4 syl ⊢ φ → x ∈ A ∧ ψ ↔ x ∈ B ∧ ψ
6 1 5 rabbida4 ⊢ φ → x ∈ A | ψ = x ∈ B | ψ