Theorem dfopif

Description: Rewrite df-op using if . When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

	Ref	Expression
Assertion	dfopif	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-op	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
2		df-3an	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
3	2	abbii	⊢ { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
4		iftrue	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = { { 𝐴 } , { 𝐴 , 𝐵 } } )
5		ibar	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
6	5	eqabdv	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } )
7	4 6	eqtr2d	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) )
8		pm2.21	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑥 ∈ ∅ ) )
9	8	adantrd	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) → 𝑥 ∈ ∅ ) )
10	9	abssdv	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } ⊆ ∅ )
11		ss0	⊢ ( { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } ⊆ ∅ → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = ∅ )
12	10 11	syl	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = ∅ )
13		iffalse	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = ∅ )
14	12 13	eqtr4d	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) )
15	7 14	pm2.61i	⊢ { 𝑥 ∣ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
16	1 3 15	3eqtri	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )