Description: Formulabuilding rule for the atmostone quantifier (inference form). (Contributed by NM, 9Mar1995) (Revised by Mario Carneiro, 17Oct2016) Avoid ax5 . (Revised by Wolf Lammen, 24Sep2023)
Ref  Expression  

Hypothesis  mobii.1   ( ps <> ch ) 

Assertion  mobii   ( E* x ps <> E* x ch ) 
Step  Hyp  Ref  Expression 

1  mobii.1   ( ps <> ch ) 

2  1  biimpri   ( ch > ps ) 
3  2  moimi   ( E* x ps > E* x ch ) 
4  1  biimpi   ( ps > ch ) 
5  4  moimi   ( E* x ch > E* x ps ) 
6  3 5  impbii   ( E* x ps <> E* x ch ) 