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

Theorem reueq1 3417
Description: Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2177. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2110. (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 3322 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
2 rmoeq1 3416 . . 3 (𝐴 = 𝐵 → (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥𝐵 𝜑))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐵 𝜑 ∧ ∃*𝑥𝐵 𝜑)))
4 reu5 3382 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
5 reu5 3382 . 2 (∃!𝑥𝐵 𝜑 ↔ (∃𝑥𝐵 𝜑 ∧ ∃*𝑥𝐵 𝜑))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wrex 3070  ∃!wreu 3378  ∃*wrmo 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-cleq 2729  df-rex 3071  df-rmo 3380  df-reu 3381
This theorem is referenced by:  reueqd  3421  reueqdv  3422  lubfval  18395  glbfval  18408  uspgredg2vlem  29240  uspgredg2v  29241  isfrgr  30279  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgr  30297  isplig  30495  hdmap14lem4a  41873  hdmap14lem15  41884
  Copyright terms: Public domain W3C validator