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

Theorem en2sn 9036
Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5353. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7718. (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 5421 . . 3 {⟨𝐴, 𝐵⟩} ∈ V
2 f1osng 6864 . . 3 ((𝐴𝐶𝐵𝐷) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
3 f1oeq1 6811 . . . 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 5421 . . 3 {𝐴} ∈ V
7 snex 5421 . . 3 {𝐵} ∈ V
8 breng 8943 . . 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 4620  cop 4626   class class class wbr 5138  1-1-ontowf1o 6532  cen 8931
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 5289  ax-nul 5296  ax-pr 5417
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 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-opab 5201  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-en 8935
This theorem is referenced by:  enrefnn  9042  enpr2dOLD  9045  difsnen  9048  domunsncan  9067  sucdom2OLD  9077  domunsn  9122  limensuci  9148  infensuc  9150  unfi  9167  sucdom2  9201  0sdom1dom  9233  1sdom2dom  9242  dif1ennnALT  9272  dif1card  10000  fin23lem26  10315  unsnen  10543  canthp1lem1  10642  fzennn  13929  hashsng  14325  mreexexlem4d  17589
  Copyright terms: Public domain W3C validator