Metamath Proof Explorer

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 ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅

Proof

Step Hyp Ref Expression
1 df-op ⊢ A B = x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B
2 df-3an ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
3 2 abbii ⊢ x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B
4 iftrue ⊢ A ∈ V ∧ B ∈ V → if A ∈ V ∧ B ∈ V A A B ∅ = A A B
5 ibar ⊢ A ∈ V ∧ B ∈ V → x ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
6 5 abbi2dv ⊢ A ∈ V ∧ B ∈ V → A A B = x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B
7 4 6 eqtr2d ⊢ A ∈ V ∧ B ∈ V → x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = if A ∈ V ∧ B ∈ V A A B ∅
8 pm2.21 ⊢ ¬ A ∈ V ∧ B ∈ V → A ∈ V ∧ B ∈ V → x ∈ ∅
9 8 adantrd ⊢ ¬ A ∈ V ∧ B ∈ V → A ∈ V ∧ B ∈ V ∧ x ∈ A A B → x ∈ ∅
10 9 abssdv ⊢ ¬ A ∈ V ∧ B ∈ V → x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B ⊆ ∅
11 ss0 ⊢ x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B ⊆ ∅ → x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = ∅
12 10 11 syl ⊢ ¬ A ∈ V ∧ B ∈ V → x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = ∅
13 iffalse ⊢ ¬ A ∈ V ∧ B ∈ V → if A ∈ V ∧ B ∈ V A A B ∅ = ∅
14 12 13 eqtr4d ⊢ ¬ A ∈ V ∧ B ∈ V → x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = if A ∈ V ∧ B ∈ V A A B ∅
15 7 14 pm2.61i ⊢ x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B = if A ∈ V ∧ B ∈ V A A B ∅
16 1 3 15 3eqtri ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅