Metamath Proof Explorer


Theorem reqabi

Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004)

Ref Expression
Hypothesis reqabi.1 A = x B | φ
Assertion reqabi x A x B φ

Proof

Step Hyp Ref Expression
1 reqabi.1 A = x B | φ
2 1 eleq2i x A x x B | φ
3 rabid x x B | φ x B φ
4 2 3 bitri x A x B φ