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

Theorem en2sn 9038
Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5354. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7719. (Revised by BTernaryTau, 25-Sep-2024.)
Assertion
Ref Expression
en2sn ((𝐴𝐶𝐵𝐷) → {𝐴} ≈ {𝐵})

Proof of Theorem en2sn
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 snex 5422 . . 3 {⟨𝐴, 𝐵⟩} ∈ V
2 f1osng 6865 . . 3 ((𝐴𝐶𝐵𝐷) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
3 f1oeq1 6812 . . . 4 (𝑓 = {⟨𝐴, 𝐵⟩} → (𝑓:{𝐴}–1-1-onto→{𝐵} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}))
43spcegv 3579 . . 3 ({⟨𝐴, 𝐵⟩} ∈ V → ({⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵} → ∃𝑓 𝑓:{𝐴}–1-1-onto→{𝐵}))
51, 2, 4mpsyl 68 . 2 ((𝐴𝐶𝐵𝐷) → ∃𝑓 𝑓:{𝐴}–1-1-onto→{𝐵})
6 snex 5422 . . 3 {𝐴} ∈ V
7 snex 5422 . . 3 {𝐵} ∈ V
8 breng 8945 . . 3 (({𝐴} ∈ V ∧ {𝐵} ∈ V) → ({𝐴} ≈ {𝐵} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{𝐵}))
96, 7, 8mp2an 689 . 2 ({𝐴} ≈ {𝐵} ↔ ∃𝑓 𝑓:{𝐴}–1-1-onto→{𝐵})
105, 9sylibr 233 1 ((𝐴𝐶𝐵𝐷) → {𝐴} ≈ {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wex 1773  wcel 2098  Vcvv 3466  {csn 4621  cop 4627   class class class wbr 5139  1-1-ontowf1o 6533  cen 8933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-mo 2526  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-br 5140  df-opab 5202  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-en 8937
This theorem is referenced by:  enrefnn  9044  enpr2dOLD  9047  difsnen  9050  domunsncan  9069  sucdom2OLD  9079  domunsn  9124  limensuci  9150  infensuc  9152  unfi  9169  sucdom2  9203  0sdom1dom  9235  1sdom2dom  9244  dif1ennnALT  9274  dif1card  10002  fin23lem26  10317  unsnen  10545  canthp1lem1  10644  fzennn  13934  hashsng  14330  mreexexlem4d  17596
  Copyright terms: Public domain W3C validator