MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfif6 Structured version   Visualization version   GIF version

Theorem dfif6 4080
Description: An alternate definition of the conditional operator df-if 4078 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
Assertion
Ref Expression
dfif6 if(𝜑, 𝐴, 𝐵) = ({𝑥𝐴𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfif6
StepHypRef Expression
1 unab 3886 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝜑)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
2 df-rab 2918 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
3 df-rab 2918 . . 3 {𝑥𝐵 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝜑)}
42, 3uneq12i 3757 . 2 ({𝑥𝐴𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝜑)})
5 df-if 4078 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
61, 4, 53eqtr4ri 2653 1 if(𝜑, 𝐴, 𝐵) = ({𝑥𝐴𝜑} ∪ {𝑥𝐵 ∣ ¬ 𝜑})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 383  wa 384   = wceq 1481  wcel 1988  {cab 2606  {crab 2913  cun 3565  ifcif 4077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-un 3572  df-if 4078
This theorem is referenced by:  ifeq1  4081  ifeq2  4082  dfif3  4091
  Copyright terms: Public domain W3C validator