Theorem enpr2 9924

Description: An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 8992. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5301, ax-un 7685. (Revised by BTernaryTau, 30-Dec-2024.)

Assertion

Ref	Expression
enpr2	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)

Proof of Theorem enpr2

Step	Hyp	Ref	Expression
1		df-ne 2936	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		simp1 1142	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ 𝐶)
3		simp2 1143	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ 𝐷)
4		simp3 1144	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
5	2, 3, 4	enpr2d 8992	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
6	1, 5	syl3an3b 1413	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)

Syntax hints:  ¬ wn 3   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  {cpr 4564   class class class wbr 5079  2_oc2o 8396   ≈ cen 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-suc 6323  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-1o 8402  df-2o 8403  df-en 8891

This theorem is referenced by:  pr2ne  9925  en2eqpr  9927  en2eleq  9928  pr2pwpr  14439  pmtrprfv  19426  pmtrprfv3  19427  symggen  19443  pmtr3ncomlem1  19446  pmtr3ncom  19448  mdetralt  22598  en2top  22975  hmphindis  23787  pmtrcnel  33177  pmtrcnel2  33178  fzo0pmtrlast  33180  pmtridf1o  33182  pmtrto1cl  33187  cycpm2tr  33207  cyc3evpm  33238  cyc3genpmlem  33239  cyc3conja  33245