Metamath Proof Explorer

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 ⊢ 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 ∅