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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = { 𝐴 } ∨ 𝐶 = { 𝐴 , 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 dfopg ( ( 𝐴𝑉𝐵𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2 eleq2 ( ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } → ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐶 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
3 snex { 𝐴 } ∈ V
4 prex { 𝐴 , 𝐵 } ∈ V
5 3 4 elpr2 ( 𝐶 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ ( 𝐶 = { 𝐴 } ∨ 𝐶 = { 𝐴 , 𝐵 } ) )
6 2 5 bitrdi ( ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } → ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = { 𝐴 } ∨ 𝐶 = { 𝐴 , 𝐵 } ) ) )
7 1 6 syl ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = { 𝐴 } ∨ 𝐶 = { 𝐴 , 𝐵 } ) ) )