Metamath Proof Explorer


Theorem brdomi

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015) Avoid ax-un . (Revised by BTernaryTau, 29-Nov-2024)

Ref Expression
Assertion brdomi ABff:A1-1B

Proof

Step Hyp Ref Expression
1 reldom Rel
2 1 brrelex12i ABAVBV
3 brdom2g AVBVABff:A1-1B
4 2 3 syl ABABff:A1-1B
5 4 ibi ABff:A1-1B