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 ax-10 , ax-11 , ax-12 . (Revised by SN, 1-Aug-2024) (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 noel ⊢ ¬ x ∈ ∅
2 1 intnan ⊢ ¬ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅
3 biorf ⊢ ¬ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅ → A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅ ∨ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
4 2 3 ax-mp ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅ ∨ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
5 df-3an ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
6 orcom ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ∨ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅ ↔ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅ ∨ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
7 4 5 6 3bitr4i ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ∨ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅
8 eleq1 ⊢ y = x → y ∈ A A B ↔ x ∈ A A B
9 8 3anbi3d ⊢ y = x → A ∈ V ∧ B ∈ V ∧ y ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
10 df-op ⊢ A B = y | A ∈ V ∧ B ∈ V ∧ y ∈ A A B
11 9 10 elab2g ⊢ x ∈ V → x ∈ A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
12 11 elv ⊢ x ∈ A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
13 elif ⊢ x ∈ if A ∈ V ∧ B ∈ V A A B ∅ ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ∨ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅
14 7 12 13 3bitr4i ⊢ x ∈ A B ↔ x ∈ if A ∈ V ∧ B ∈ V A A B ∅
15 14 eqriv ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅