Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23Nov1994) (Revised by Mario Carneiro, 17Oct2016) (Proof shortened by Wolf Lammen, 4Dec2019)
Ref  Expression  

Hypothesis  ralbii.1   ( ph <> ps ) 

Assertion  ralbii   ( A. x e. A ph <> A. x e. A ps ) 
Step  Hyp  Ref  Expression 

1  ralbii.1   ( ph <> ps ) 

2  1  imbi2i   ( ( x e. A > ph ) <> ( x e. A > ps ) ) 
3  2  ralbii2   ( A. x e. A ph <> A. x e. A ps ) 