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

Theorem reubii 3105
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 3104 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wcel 1977  ∃!wreu 2898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-reu 2903
This theorem is referenced by:  2reu5lem1  3380  reusv2lem5  4799  reusv2  4800  oaf1o  7530  aceq2  8825  lubfval  16801  lubeldm  16804  glbfval  16814  glbeldm  16817  oduglb  16962  odulub  16964  usgraidx2vlem1  25920  usgraidx2vlem2  25921  frgraunss  26522  frgraun  26523  n4cyclfrgra  26545  cnlnadjlem3  28312  disjrdx  28786  lshpsmreu  33414  2reu7  39840  2reu8  39841  usgredg2vlem1  40452  usgredg2vlem2  40453  frcond1  41438  frcond2  41439  n4cyclfrgr  41461
  Copyright terms: Public domain W3C validator