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

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

Proof of Theorem reubii
StepHypRef Expression
1 reubii.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32reubiia 3266 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∈ wcel 2139  ∃!wreu 3052 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196 This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-eu 2611  df-reu 3057 This theorem is referenced by:  2reu5lem1  3554  reusv2lem5  5022  reusv2  5023  oaf1o  7814  aceq2  9152  lubfval  17199  lubeldm  17202  glbfval  17212  glbeldm  17215  oduglb  17360  odulub  17362  usgredg2vlem1  26337  usgredg2vlem2  26338  frcond1  27441  frcond2  27442  n4cyclfrgr  27466  cnlnadjlem3  29258  disjrdx  29732  lshpsmreu  34917  2reu7  41715  2reu8  41716
 Copyright terms: Public domain W3C validator