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

Theorem reubii 3366
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 3364 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wcel 2132  ∃!wreu 3355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-mo 2556  df-eu 2586  df-reu 3358
This theorem is referenced by:  2reu5lem1  3708  reusv2lem5  5349  reusv2  5350  oaf1o  8516  aceq2  10061  lubfval  18352  lubeldm  18355  glbfval  18365  glbeldm  18368  odulub  18409  oduglb  18411  2sqreu  27486  2sqreunn  27487  2sqreult  27488  2sqreultb  27489  2sqreunnlt  27490  2sqreunnltb  27491  uspgredgiedg  29311  uspgriedgedg  29312  usgredg2vlem1  29361  usgredg2vlem2  29362  frcond1  30403  frcond2  30404  n4cyclfrgr  30428  cnlnadjlem3  32207  disjrdx  32729  ply1divalg3  35930  lshpsmreu  39671  reuf1odnf  47639  reuf1od  47640  2reu7  47643  2reu8  47644  2reu8i  47645  2reuimp0  47646  isuspgrim0  48454  isuspgrimlem  48455  uptr2  49780
  Copyright terms: Public domain W3C validator