# Metamath Proof Explorer

## Theorem reueq1

Description: Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023)

Ref Expression
Assertion reueq1 ${⊢}{A}={B}\to \left(\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 eleq2 ${⊢}{A}={B}\to \left({x}\in {A}↔{x}\in {B}\right)$
2 1 anbi1d ${⊢}{A}={B}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({x}\in {B}\wedge {\phi }\right)\right)$
3 2 eubidv ${⊢}{A}={B}\to \left(\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)\right)$
4 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
5 df-reu ${⊢}\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)$
6 3 4 5 3bitr4g ${⊢}{A}={B}\to \left(\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$