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

Theorem ensn1g 8594
 Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
Assertion
Ref Expression
ensn1g (𝐴𝑉 → {𝐴} ≈ 1o)

Proof of Theorem ensn1g
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sneq 4533 . . 3 (𝑥 = 𝐴 → {𝑥} = {𝐴})
21breq1d 5043 . 2 (𝑥 = 𝐴 → ({𝑥} ≈ 1o ↔ {𝐴} ≈ 1o))
3 vex 3414 . . 3 𝑥 ∈ V
43ensn1 8593 . 2 {𝑥} ≈ 1o
52, 4vtoclg 3486 1 (𝐴𝑉 → {𝐴} ≈ 1o)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  {csn 4523   class class class wbr 5033  1oc1o 8106   ≈ cen 8525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-suc 6176  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-1o 8113  df-en 8529 This theorem is referenced by:  enpr1g  8595  en1b  8597  snmapen1  8611  en2snOLD  8614  snfi  8615  enpr2d  8618  snnen2o  8729  sucxpdom  8749  en1eqsn  8770  en1eqsnbi  8771  pr2nelem  9457  prdom2  9459  dju1en  9624  triv1nsgd  18385  snct  30565  rngoueqz  35651  sn1dom  40600
 Copyright terms: Public domain W3C validator