MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mobii Structured version   Unicode version

Theorem mobii 2318
Description: Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
Hypothesis
Ref Expression
mobii.1  |-  ( ps  <->  ch )
Assertion
Ref Expression
mobii  |-  ( E* x ps  <->  E* x ch )

Proof of Theorem mobii
StepHypRef Expression
1 mobii.1 . . . 4  |-  ( ps  <->  ch )
21a1i 11 . . 3  |-  (  T. 
->  ( ps  <->  ch )
)
32mobidv 2317 . 2  |-  (  T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1333 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    T. wtru 1326   E*wmo 2283
This theorem is referenced by:  moaneu  2341  moanmo  2342  2moswap  2357  2eu1  2362  rmobiia  2899  rmov  2973  euxfr2  3120  rmoan  3133  2reu5lem2  3141  reuxfr2d  4747  dffun9  5482  funopab  5487  funcnv2  5511  funcnv  5512  fun2cnv  5514  fncnv  5516  imadif  5529  fnres  5562  oprabex3  6189  ov3  6211  brdom6disj  8411  grothprim  8710  axaddf  9021  axmulf  9022  spwmo  14659  reuxfr3d  23977  funcnvmptOLD  24083  funcnvmpt  24084  2rmoswap  27939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-tru 1329  df-ex 1552  df-nf 1555  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator