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 ax-10 , ax-11 , ax-12 . (Revised by SN, 1-Aug-2024) (Avoid depending on this detail.)

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

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑥 ∈ ∅
2	1	intnan	⊢ ¬ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ )
3		biorf	⊢ ( ¬ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ∨ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) ) )
4	2 3	ax-mp	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ∨ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
5		df-3an	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
6		orcom	⊢ ( ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ∨ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ) ↔ ( ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ∨ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
7	4 5 6	3bitr4i	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ∨ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ) )
8		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ 𝑦 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
9	8	3anbi3d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑦 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
10		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
11	10	3anbi3d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑦 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
12		df-op	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
13	9 11 12	elab2gw	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ) )
14	13	elv	⊢ ( 𝑥 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
15		elif	⊢ ( 𝑥 ∈ if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) ↔ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) ∨ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑥 ∈ ∅ ) ) )
16	7 14 15	3bitr4i	⊢ ( 𝑥 ∈ ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ∈ if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) )
17	16	eqriv	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )