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 eleq1w ⊢ x = y → x ∈ A A B ↔ y ∈ A A B
9 8 3anbi3d ⊢ x = y → A ∈ V ∧ B ∈ V ∧ x ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ y ∈ A A B
10 eleq1w ⊢ y = x → y ∈ A A B ↔ x ∈ A A B
11 10 3anbi3d ⊢ y = x → A ∈ V ∧ B ∈ V ∧ y ∈ A A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
12 df-op ⊢ A B = x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B
13 9 11 12 elab2gw ⊢ x ∈ V → x ∈ A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
14 13 elv ⊢ x ∈ A B ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B
15 elif ⊢ x ∈ if A ∈ V ∧ B ∈ V A A B ∅ ↔ A ∈ V ∧ B ∈ V ∧ x ∈ A A B ∨ ¬ A ∈ V ∧ B ∈ V ∧ x ∈ ∅
16 7 14 15 3bitr4i ⊢ x ∈ A B ↔ x ∈ if A ∈ V ∧ B ∈ V A A B ∅
17 16 eqriv ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅