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