Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-dfifc2 Structured version   Visualization version   GIF version

Theorem bj-dfifc2 33459
 Description: This should be the alternate definition of "ifc" if "if-" enters the main part. (Contributed by BJ, 20-Sep-2019.)
Assertion
Ref Expression
bj-dfifc2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝜑𝑥𝐴) ∨ (¬ 𝜑𝑥𝐵))}
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵

Proof of Theorem bj-dfifc2
StepHypRef Expression
1 df-if 4345 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
2 ancom 453 . . . . 5 ((𝜑𝑥𝐴) ↔ (𝑥𝐴𝜑))
3 ancom 453 . . . . 5 ((¬ 𝜑𝑥𝐵) ↔ (𝑥𝐵 ∧ ¬ 𝜑))
42, 3orbi12i 898 . . . 4 (((𝜑𝑥𝐴) ∨ (¬ 𝜑𝑥𝐵)) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑)))
54bicomi 216 . . 3 (((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑)) ↔ ((𝜑𝑥𝐴) ∨ (¬ 𝜑𝑥𝐵)))
65abbii 2838 . 2 {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))} = {𝑥 ∣ ((𝜑𝑥𝐴) ∨ (¬ 𝜑𝑥𝐵))}
71, 6eqtri 2796 1 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝜑𝑥𝐴) ∨ (¬ 𝜑𝑥𝐵))}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2050  {cab 2752  ifcif 4344 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2744 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2016  df-clab 2753  df-cleq 2765  df-if 4345 This theorem is referenced by:  bj-df-ifc  33460
 Copyright terms: Public domain W3C validator