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

Theorem mobii 2192
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 10 . . 3  |-  (  T. 
->  ( ps  <->  ch )
)
32mobidv 2191 . 2  |-  (  T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1314 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307   E*wmo 2157
This theorem is referenced by:  moaneu  2215  moanmo  2216  2moswap  2231  2eu1  2236  rmobiia  2743  rmov  2817  euxfr2  2963  rmoan  2976  2reu5lem2  2984  reuxfr2d  4573  dffun9  5298  funopab  5303  funcnv2  5325  funcnv  5326  fun2cnv  5328  fncnv  5330  imadif  5343  fnres  5376  oprabex3  5978  ov3  6000  brdom6disj  8173  grothprim  8472  axaddf  8783  axmulf  8784  spwmo  14351  reuxfr3d  23154  funcnvmptOLD  23249  funcnvmpt  23250  2rmoswap  28064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1532  df-nf 1535  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator