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 ⊢AB=ifA∈V∧B∈VAAB∅

Proof

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