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

Theorem reubii 3376
Description: Formula-building rule for restricted existential quantifier (inference form). (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 3375 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2115  ∃!wreu 3128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2623  df-eu 2654  df-reu 3133
This theorem is referenced by:  2reu5lem1  3723  reusv2lem5  5276  reusv2  5277  oaf1o  8164  aceq2  9522  lubfval  17567  lubeldm  17570  glbfval  17580  glbeldm  17583  oduglb  17728  odulub  17730  2sqreu  26019  2sqreunn  26020  2sqreult  26021  2sqreultb  26022  2sqreunnlt  26023  2sqreunnltb  26024  usgredg2vlem1  26994  usgredg2vlem2  26995  frcond1  28030  frcond2  28031  n4cyclfrgr  28055  cnlnadjlem3  29831  disjrdx  30328  lshpsmreu  36287  reuf1odnf  43482  reuf1od  43483  2reu7  43486  2reu8  43487  2reu8i  43488  2reuimp0  43489
  Copyright terms: Public domain W3C validator