New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > dfif3 | GIF version |
Description: Alternate definition of the conditional operator df-if 3664. Note that φ is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Ref | Expression |
---|---|
dfif3.1 | ⊢ C = {x ∣ φ} |
Ref | Expression |
---|---|
dfif3 | ⊢ if(φ, A, B) = ((A ∩ C) ∪ (B ∩ (V ∖ C))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfif6 3666 | . 2 ⊢ if(φ, A, B) = ({y ∈ A ∣ φ} ∪ {y ∈ B ∣ ¬ φ}) | |
2 | dfif3.1 | . . . . . 6 ⊢ C = {x ∣ φ} | |
3 | biidd 228 | . . . . . . 7 ⊢ (x = y → (φ ↔ φ)) | |
4 | 3 | cbvabv 2473 | . . . . . 6 ⊢ {x ∣ φ} = {y ∣ φ} |
5 | 2, 4 | eqtri 2373 | . . . . 5 ⊢ C = {y ∣ φ} |
6 | 5 | ineq2i 3455 | . . . 4 ⊢ (A ∩ C) = (A ∩ {y ∣ φ}) |
7 | dfrab3 3532 | . . . 4 ⊢ {y ∈ A ∣ φ} = (A ∩ {y ∣ φ}) | |
8 | 6, 7 | eqtr4i 2376 | . . 3 ⊢ (A ∩ C) = {y ∈ A ∣ φ} |
9 | dfrab3 3532 | . . . 4 ⊢ {y ∈ B ∣ ¬ φ} = (B ∩ {y ∣ ¬ φ}) | |
10 | notab 3526 | . . . . . 6 ⊢ {y ∣ ¬ φ} = (V ∖ {y ∣ φ}) | |
11 | 5 | difeq2i 3383 | . . . . . 6 ⊢ (V ∖ C) = (V ∖ {y ∣ φ}) |
12 | 10, 11 | eqtr4i 2376 | . . . . 5 ⊢ {y ∣ ¬ φ} = (V ∖ C) |
13 | 12 | ineq2i 3455 | . . . 4 ⊢ (B ∩ {y ∣ ¬ φ}) = (B ∩ (V ∖ C)) |
14 | 9, 13 | eqtr2i 2374 | . . 3 ⊢ (B ∩ (V ∖ C)) = {y ∈ B ∣ ¬ φ} |
15 | 8, 14 | uneq12i 3417 | . 2 ⊢ ((A ∩ C) ∪ (B ∩ (V ∖ C))) = ({y ∈ A ∣ φ} ∪ {y ∈ B ∣ ¬ φ}) |
16 | 1, 15 | eqtr4i 2376 | 1 ⊢ if(φ, A, B) = ((A ∩ C) ∪ (B ∩ (V ∖ C))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1642 {cab 2339 {crab 2619 Vcvv 2860 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ifcif 3663 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-rab 2624 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-if 3664 |
This theorem is referenced by: dfif4 3674 |
Copyright terms: Public domain | W3C validator |