Metamath Proof Explorer

Theorem eleq1d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993) Allow shortening of eleq1 . (Revised by Wolf Lammen, 20-Nov-2019)

Ref Expression
Hypothesis eleq1d.1 φ A = B
Assertion eleq1d φ A C B C


Step Hyp Ref Expression
1 eleq1d.1 φ A = B
2 1 eqeq2d φ x = A x = B
3 2 anbi1d φ x = A x C x = B x C
4 3 exbidv φ x x = A x C x x = B x C
5 dfclel A C x x = A x C
6 dfclel B C x x = B x C
7 4 5 6 3bitr4g φ A C B C