Theorem moeq 3349

Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)

Assertion

Ref	Expression
moeq	⊢ ∃*𝑥 𝑥 = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem moeq

Step	Hyp	Ref	Expression
1		isset 3180	. . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
2		eueq 3345	. . 3 ⊢ (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)
3	1, 2	sylbb1 226	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)
4		df-mo 2463	. 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴))
5	3, 4	mpbir 220	1 ⊢ ∃*𝑥 𝑥 = 𝐴

Syntax hints:   → wi 4   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  ∃*wmo 2459  Vcvv 3173

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-13 2234  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-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  mosub  3351  euxfr2  3358  reueq  3371  rmoeq  3372  sndisj  4574  disjxsn  4576  reusv1OLD  4793  reuxfr2d  4817  funopabeq  5838  funcnvsn  5850  fvmptg  6189  fvopab6  6218  ovmpt4g  6681  ov3  6695  ov6g  6696  oprabex3  7048  1stconst  7152  2ndconst  7153  iunmapdisj  8729  axaddf  9845  axmulf  9846  joinfval  16824  joinval  16828  meetfval  16838  meetval  16842  reuxfr3d  28713  abrexdom2jm  28730  abrexdom2  32696