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

Theorem reueq1 3116
Description: Equality theorem for restricted uniqueness quantifier. (Contributed by NM, 5-Apr-2004.)
Assertion
Ref Expression
reueq1 (𝐴 = 𝐵 → (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reueq1
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝐴
2 nfcv 2750 . 2 𝑥𝐵
31, 2reueq1f 3112 1 (𝐴 = 𝐵 → (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  ∃!wreu 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-eu 2461  df-cleq 2602  df-clel 2605  df-nfc 2739  df-reu 2902
This theorem is referenced by:  reueqd  3124  lubfval  16747  glbfval  16760  isfrgra  26283  frgra3v  26295  1vwmgra  26296  3vfriswmgra  26298  isplig  26486  hdmap14lem4a  35984  hdmap14lem15  35995  uspgredg2vlem  40452  uspgredg2v  40453  frgr1v  41443  nfrgr2v  41444  frgr3v  41447  1vwmgr  41448  3vfriswmgr  41450
  Copyright terms: Public domain W3C validator