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

Theorem mobii 2290
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 2289 . 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 2255
This theorem is referenced by:  moaneu  2313  moanmo  2314  2moswap  2329  2eu1  2334  rmobiia  2858  rmov  2932  euxfr2  3079  rmoan  3092  2reu5lem2  3100  reuxfr2d  4705  dffun9  5440  funopab  5445  funcnv2  5469  funcnv  5470  fun2cnv  5472  fncnv  5474  imadif  5487  fnres  5520  oprabex3  6147  ov3  6169  brdom6disj  8366  grothprim  8665  axaddf  8976  axmulf  8977  spwmo  14613  reuxfr3d  23929  funcnvmptOLD  24035  funcnvmpt  24036  2rmoswap  27829
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 2258  df-mo 2259
  Copyright terms: Public domain W3C validator