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

Theorem mobii 2179
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 2178 . 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 2144
This theorem is referenced by:  moaneu  2202  moanmo  2203  2moswap  2218  2eu1  2223  rmobiia  2730  rmov  2804  euxfr2  2950  rmoan  2963  2reu5lem2  2971  reuxfr2d  4557  dffun9  5282  funopab  5287  funcnv2  5309  funcnv  5310  fun2cnv  5312  fncnv  5314  imadif  5327  fnres  5360  oprabex3  5962  ov3  5984  brdom6disj  8157  grothprim  8456  axaddf  8767  axmulf  8768  spwmo  14335  reuxfr3d  23138  funcnvmptOLD  23234  funcnvmpt  23235  2rmoswap  27962
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1529  df-nf 1532  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator