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

Theorem enpr2 10040
Description: An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 9088. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5371, ax-un 7754. (Revised by BTernaryTau, 30-Dec-2024.)
Assertion
Ref Expression
enpr2 ((𝐴𝐶𝐵𝐷𝐴𝐵) → {𝐴, 𝐵} ≈ 2o)

Proof of Theorem enpr2
StepHypRef Expression
1 df-ne 2939 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 simp1 1135 . . 3 ((𝐴𝐶𝐵𝐷 ∧ ¬ 𝐴 = 𝐵) → 𝐴𝐶)
3 simp2 1136 . . 3 ((𝐴𝐶𝐵𝐷 ∧ ¬ 𝐴 = 𝐵) → 𝐵𝐷)
4 simp3 1137 . . 3 ((𝐴𝐶𝐵𝐷 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
52, 3, 4enpr2d 9088 . 2 ((𝐴𝐶𝐵𝐷 ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
61, 5syl3an3b 1404 1 ((𝐴𝐶𝐵𝐷𝐴𝐵) → {𝐴, 𝐵} ≈ 2o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  w3a 1086   = wceq 1537  wcel 2106  wne 2938  {cpr 4633   class class class wbr 5148  2oc2o 8499  cen 8981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-suc 6392  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-1o 8505  df-2o 8506  df-en 8985
This theorem is referenced by:  pr2ne  10042  pr2neOLD  10043  en2eqpr  10045  en2eleq  10046  pr2pwpr  14515  pmtrprfv  19486  pmtrprfv3  19487  symggen  19503  pmtr3ncomlem1  19506  pmtr3ncom  19508  mdetralt  22630  en2top  23008  hmphindis  23821  pmtrcnel  33092  pmtrcnel2  33093  fzo0pmtrlast  33095  pmtridf1o  33097  pmtrto1cl  33102  cycpm2tr  33122  cyc3evpm  33153  cyc3genpmlem  33154  cyc3conja  33160
  Copyright terms: Public domain W3C validator