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

Theorem mobii 2323
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 2322 . 2  |-  (  T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1333 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    T. wtru 1326   E*wmo 2288
This theorem is referenced by:  moaneu  2346  moanmo  2347  2moswap  2362  2eu1  2367  rmobiia  2904  rmov  2978  euxfr2  3125  rmoan  3138  2reu5lem2  3146  reuxfr2d  4775  dffun9  5510  funopab  5515  funcnv2  5539  funcnv  5540  fun2cnv  5542  fncnv  5544  imadif  5557  fnres  5590  oprabex3  6217  ov3  6239  brdom6disj  8441  grothprim  8740  axaddf  9051  axmulf  9052  spwmo  14689  reuxfr3d  24007  funcnvmptOLD  24113  funcnvmpt  24114  2rmoswap  27976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-tru 1329  df-ex 1552  df-nf 1555  df-eu 2291  df-mo 2292
  Copyright terms: Public domain W3C validator