# Metamath Proof Explorer

## Theorem brsdom

Description: Strict dominance relation, meaning " B is strictly greater in size than A ". Definition of Mendelson p. 255. (Contributed by NM, 25-Jun-1998)

Ref Expression
Assertion brsdom ${⊢}{A}\prec {B}↔\left({A}\preccurlyeq {B}\wedge ¬{A}\approx {B}\right)$

### Proof

Step Hyp Ref Expression
1 df-sdom ${⊢}\prec =\preccurlyeq \setminus \approx$
2 1 eleq2i ${⊢}⟨{A},{B}⟩\in \prec ↔⟨{A},{B}⟩\in \left(\preccurlyeq \setminus \approx \right)$
3 df-br ${⊢}{A}\prec {B}↔⟨{A},{B}⟩\in \prec$
4 df-br ${⊢}{A}\preccurlyeq {B}↔⟨{A},{B}⟩\in \preccurlyeq$
5 df-br ${⊢}{A}\approx {B}↔⟨{A},{B}⟩\in \approx$
6 5 notbii ${⊢}¬{A}\approx {B}↔¬⟨{A},{B}⟩\in \approx$
7 4 6 anbi12i ${⊢}\left({A}\preccurlyeq {B}\wedge ¬{A}\approx {B}\right)↔\left(⟨{A},{B}⟩\in \preccurlyeq \wedge ¬⟨{A},{B}⟩\in \approx \right)$
8 eldif ${⊢}⟨{A},{B}⟩\in \left(\preccurlyeq \setminus \approx \right)↔\left(⟨{A},{B}⟩\in \preccurlyeq \wedge ¬⟨{A},{B}⟩\in \approx \right)$
9 7 8 bitr4i ${⊢}\left({A}\preccurlyeq {B}\wedge ¬{A}\approx {B}\right)↔⟨{A},{B}⟩\in \left(\preccurlyeq \setminus \approx \right)$
10 2 3 9 3bitr4i ${⊢}{A}\prec {B}↔\left({A}\preccurlyeq {B}\wedge ¬{A}\approx {B}\right)$