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

Theorem mobii 2298
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 2297 . 2  |-  (  T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1329 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1322   E*wmo 2263
This theorem is referenced by:  moaneu  2321  moanmo  2322  2moswap  2337  2eu1  2342  rmobiia  2866  rmov  2940  euxfr2  3087  rmoan  3100  2reu5lem2  3108  reuxfr2d  4713  dffun9  5448  funopab  5453  funcnv2  5477  funcnv  5478  fun2cnv  5480  fncnv  5482  imadif  5495  fnres  5528  oprabex3  6155  ov3  6177  brdom6disj  8374  grothprim  8673  axaddf  8984  axmulf  8985  spwmo  14621  reuxfr3d  23937  funcnvmptOLD  24043  funcnvmpt  24044  2rmoswap  27837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-tru 1325  df-ex 1548  df-nf 1551  df-eu 2266  df-mo 2267
  Copyright terms: Public domain W3C validator