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

Theorem mobii 2267
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 2266 . 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 2232
This theorem is referenced by:  moaneu  2290  moanmo  2291  2moswap  2306  2eu1  2311  rmobiia  2834  rmov  2908  euxfr2  3055  rmoan  3068  2reu5lem2  3076  reuxfr2d  4679  dffun9  5414  funopab  5419  funcnv2  5443  funcnv  5444  fun2cnv  5446  fncnv  5448  imadif  5461  fnres  5494  oprabex3  6120  ov3  6142  brdom6disj  8336  grothprim  8635  axaddf  8946  axmulf  8947  spwmo  14578  reuxfr3d  23813  funcnvmptOLD  23916  funcnvmpt  23917  2rmoswap  27623
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 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-tru 1325  df-ex 1548  df-nf 1551  df-eu 2235  df-mo 2236
  Copyright terms: Public domain W3C validator