# Metamath Proof Explorer

## Theorem brdomain

Description: Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brdomain.1 ${⊢}{A}\in \mathrm{V}$
brdomain.2 ${⊢}{B}\in \mathrm{V}$
Assertion brdomain ${⊢}{A}\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}{B}↔{B}=\mathrm{dom}{A}$

### Proof

Step Hyp Ref Expression
1 brdomain.1 ${⊢}{A}\in \mathrm{V}$
2 brdomain.2 ${⊢}{B}\in \mathrm{V}$
3 1 2 brimage ${⊢}{A}\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right){B}↔{B}=\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)\left[{A}\right]$
4 df-domain ${⊢}\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)$
5 4 breqi ${⊢}{A}\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}{B}↔{A}\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right){B}$
6 dfdm5 ${⊢}\mathrm{dom}{A}=\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)\left[{A}\right]$
7 6 eqeq2i ${⊢}{B}=\mathrm{dom}{A}↔{B}=\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)\left[{A}\right]$
8 3 5 7 3bitr4i ${⊢}{A}\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}{B}↔{B}=\mathrm{dom}{A}$