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

Theorem mobii 2265
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 2263 . 2  |-  ( T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1416 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 186   T. wtru 1408   E*wmo 2241
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-12 1880
This theorem depends on definitions:  df-bi 187  df-tru 1410  df-ex 1636  df-nf 1640  df-eu 2244  df-mo 2245
This theorem is referenced by:  moanmo  2306  2moswap  2322  2eu1OLD  2330  rmobiia  3000  rmov  3078  euxfr2  3236  rmoan  3250  2reu5lem2  3258  reuxfr2d  4616  dffun9  5599  funopab  5604  funcnv2  5630  funcnv  5631  fun2cnv  5633  fncnv  5635  imadif  5646  fnres  5680  ov3  6422  oprabex3  6775  brdom6disj  8944  grothprim  9244  axaddf  9554  axmulf  9555  reuxfr3d  27816  funcnvmptOLD  27965  funcnvmpt  27966  2rmoswap  37570
  Copyright terms: Public domain W3C validator