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

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
3		dfopif	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
4		iftrue	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = { { 𝐴 } , { 𝐴 , 𝐵 } } )
5	3 4	syl5eq	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
6	1 2 5	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )