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

Theorem bren2 8518
 Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)
Assertion
Ref Expression
bren2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))

Proof of Theorem bren2
StepHypRef Expression
1 endom 8514 . . 3 (𝐴𝐵𝐴𝐵)
2 sdomnen 8516 . . . 4 (𝐴𝐵 → ¬ 𝐴𝐵)
32con2i 141 . . 3 (𝐴𝐵 → ¬ 𝐴𝐵)
41, 3jca 514 . 2 (𝐴𝐵 → (𝐴𝐵 ∧ ¬ 𝐴𝐵))
5 brdom2 8517 . . . 4 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
65biimpi 218 . . 3 (𝐴𝐵 → (𝐴𝐵𝐴𝐵))
76orcanai 999 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) → 𝐴𝐵)
84, 7impbii 211 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∨ wo 843   class class class wbr 5042   ≈ cen 8484   ≼ cdom 8485   ≺ csdm 8486 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-xp 5537  df-rel 5538  df-f1o 6338  df-en 8488  df-dom 8489  df-sdom 8490 This theorem is referenced by:  marypha1lem  8875  tskwe  9357  infxpenlem  9417  cdainflem  9591  axcclem  9857  alephsuc3  9980  gchen1  10025  gchen2  10026  inatsk  10178  ufilen  22514  dirith2  26091  f1ocnt  30512  lindsenlbs  34928  mblfinlem1  34970  axccdom  41641  axccd2  41650
 Copyright terms: Public domain W3C validator