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

Theorem mobii 2245
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 2244 . 2  |-  (  T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1323 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1316   E*wmo 2210
This theorem is referenced by:  moaneu  2268  moanmo  2269  2moswap  2284  2eu1  2289  rmobiia  2806  rmov  2880  euxfr2  3026  rmoan  3039  2reu5lem2  3047  reuxfr2d  4639  dffun9  5364  funopab  5369  funcnv2  5391  funcnv  5392  fun2cnv  5394  fncnv  5396  imadif  5409  fnres  5442  oprabex3  6049  ov3  6071  brdom6disj  8247  grothprim  8546  axaddf  8857  axmulf  8858  spwmo  14434  reuxfr3d  23171  funcnvmptOLD  23285  funcnvmpt  23286  2rmoswap  27285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-tru 1319  df-ex 1542  df-nf 1545  df-eu 2213  df-mo 2214
  Copyright terms: Public domain W3C validator