Theorem dfopifOLD

Description: Obsolete version of dfopif as of 1-Aug-2024. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	dfopifOLD	⊢ ⟨ 𝐴 , 𝐵 ⟩ = 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	abbi2dv	⊢ ( ( 𝐴 ∈ 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 ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )