# Metamath Proof Explorer

## Theorem dfopg

Description: Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

Ref Expression
Assertion dfopg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to ⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
2 elex ${⊢}{B}\in {W}\to {B}\in \mathrm{V}$
3 dfopif ${⊢}⟨{A},{B}⟩=if\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\},\varnothing \right)$
4 iftrue ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to if\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\},\varnothing \right)=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$
5 3 4 syl5eq ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to ⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$
6 1 2 5 syl2an ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to ⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$