Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26Nov2000)
Ref  Expression  

Hypothesis  ralbiia.1   ( x e. A > ( ph <> ps ) ) 

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

1  ralbiia.1   ( x e. A > ( ph <> ps ) ) 

2  1  pm5.74i   ( ( x e. A > ph ) <> ( x e. A > ps ) ) 
3  2  ralbii2   ( A. x e. A ph <> A. x e. A ps ) 