Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reueq1 | Structured version Visualization version GIF version |
Description: Equality theorem for restricted uniqueness quantifier. (Contributed by NM, 5-Apr-2004.) |
Ref | Expression |
---|---|
reueq1 | ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | reueq1f 3113 | 1 ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∃!wreu 2898 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-eu 2462 df-cleq 2603 df-clel 2606 df-nfc 2740 df-reu 2903 |
This theorem is referenced by: reueqd 3125 lubfval 16801 glbfval 16814 isfrgra 26517 frgra3v 26529 1vwmgra 26530 3vfriswmgra 26532 isplig 26720 hdmap14lem4a 36181 hdmap14lem15 36192 uspgredg2vlem 40450 uspgredg2v 40451 frgr1v 41441 nfrgr2v 41442 frgr3v 41445 1vwmgr 41446 3vfriswmgr 41448 |
Copyright terms: Public domain | W3C validator |