# Metamath Proof Explorer

## Theorem elopg

Description: Characterization of the elements of an ordered pair. Closed form of elop . (Contributed by BJ, 22-Jun-2019) (Avoid depending on this detail.)

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

### Proof

Step Hyp Ref Expression
1 dfopg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to ⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$
2 eleq2 ${⊢}⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}\to \left({C}\in ⟨{A},{B}⟩↔{C}\in \left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}\right)$
3 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
4 prex ${⊢}\left\{{A},{B}\right\}\in \mathrm{V}$
5 3 4 elpr2 ${⊢}{C}\in \left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}↔\left({C}=\left\{{A}\right\}\vee {C}=\left\{{A},{B}\right\}\right)$
6 2 5 syl6bb ${⊢}⟨{A},{B}⟩=\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}\to \left({C}\in ⟨{A},{B}⟩↔\left({C}=\left\{{A}\right\}\vee {C}=\left\{{A},{B}\right\}\right)\right)$
7 1 6 syl ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({C}\in ⟨{A},{B}⟩↔\left({C}=\left\{{A}\right\}\vee {C}=\left\{{A},{B}\right\}\right)\right)$