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

Theorem reueq1 3415
Description: Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2139, ax-11 2155, and ax-12 2175. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2108. (Revised by Wolf Lammen, 12-Mar-2025.)
Assertion
Ref Expression
reueq1 (𝐴 = 𝐵 → (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reueq1
StepHypRef Expression
1 rexeq 3320 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
2 rmoeq1 3414 . . 3 (𝐴 = 𝐵 → (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥𝐵 𝜑))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐵 𝜑 ∧ ∃*𝑥𝐵 𝜑)))
4 reu5 3380 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
5 reu5 3380 . 2 (∃!𝑥𝐵 𝜑 ↔ (∃𝑥𝐵 𝜑 ∧ ∃*𝑥𝐵 𝜑))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wrex 3068  ∃!wreu 3376  ∃*wrmo 3377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-mo 2538  df-eu 2567  df-cleq 2727  df-rex 3069  df-rmo 3378  df-reu 3379
This theorem is referenced by:  reueqd  3419  reueqdv  3420  lubfval  18408  glbfval  18421  uspgredg2vlem  29255  uspgredg2v  29256  isfrgr  30289  frgr1v  30300  nfrgr2v  30301  frgr3v  30304  1vwmgr  30305  3vfriswmgr  30307  isplig  30505  hdmap14lem4a  41854  hdmap14lem15  41865
  Copyright terms: Public domain W3C validator