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

Theorem reubii 3123
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 3122 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1988  ∃!wreu 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-eu 2472  df-reu 2916
This theorem is referenced by:  2reu5lem1  3407  reusv2lem5  4864  reusv2  4865  oaf1o  7628  aceq2  8927  lubfval  16959  lubeldm  16962  glbfval  16972  glbeldm  16975  oduglb  17120  odulub  17122  usgredg2vlem1  26098  usgredg2vlem2  26099  frcond1  27110  frcond2  27111  n4cyclfrgr  27135  cnlnadjlem3  28898  disjrdx  29376  lshpsmreu  34215  2reu7  40954  2reu8  40955
  Copyright terms: Public domain W3C validator