MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reubii Structured version   Visualization version   GIF version

Theorem reubii 3389
Description: Formula-building rule for restricted existential uniqueness quantifier (inference form). (Contributed by NM, 22-Oct-1999.)
Hypothesis
Ref Expression
rmobii.1 (𝜑𝜓)
Assertion
Ref Expression
reubii (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)

Proof of Theorem reubii
StepHypRef Expression
1 rmobii.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32reubiia 3387 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2108  ∃!wreu 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-reu 3381
This theorem is referenced by:  2reu5lem1  3761  reusv2lem5  5402  reusv2  5403  oaf1o  8601  aceq2  10159  lubfval  18395  lubeldm  18398  glbfval  18408  glbeldm  18411  odulub  18452  oduglb  18454  2sqreu  27500  2sqreunn  27501  2sqreult  27502  2sqreultb  27503  2sqreunnlt  27504  2sqreunnltb  27505  uspgredgiedg  29192  uspgriedgedg  29193  usgredg2vlem1  29242  usgredg2vlem2  29243  frcond1  30285  frcond2  30286  n4cyclfrgr  30310  cnlnadjlem3  32088  disjrdx  32604  ply1divalg3  35647  lshpsmreu  39110  reuf1odnf  47119  reuf1od  47120  2reu7  47123  2reu8  47124  2reu8i  47125  2reuimp0  47126  isuspgrim0  47872  isuspgrimlem  47874
  Copyright terms: Public domain W3C validator