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

Theorem bj-ififc 33812
Description: A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on 𝑋: it is implied by either side. (Contributed by BJ, 24-Sep-2019.) Generalize statement from setvar 𝑥 to class 𝑋. (Revised by BJ, 26-Dec-2023.)
Assertion
Ref Expression
bj-ififc (𝑋 ∈ if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝑋𝐴, 𝑋𝐵))

Proof of Theorem bj-ififc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 bj-df-ifc 33810 . . 3 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ if-(𝜑, 𝑥𝐴, 𝑥𝐵)}
21eleq2i 2901 . 2 (𝑋 ∈ if(𝜑, 𝐴, 𝐵) ↔ 𝑋 ∈ {𝑥 ∣ if-(𝜑, 𝑥𝐴, 𝑥𝐵)})
3 df-ifp 1055 . . . 4 (if-(𝜑, 𝑋𝐴, 𝑋𝐵) ↔ ((𝜑𝑋𝐴) ∨ (¬ 𝜑𝑋𝐵)))
4 elex 3510 . . . . . 6 (𝑋𝐴𝑋 ∈ V)
54adantl 482 . . . . 5 ((𝜑𝑋𝐴) → 𝑋 ∈ V)
6 elex 3510 . . . . . 6 (𝑋𝐵𝑋 ∈ V)
76adantl 482 . . . . 5 ((¬ 𝜑𝑋𝐵) → 𝑋 ∈ V)
85, 7jaoi 851 . . . 4 (((𝜑𝑋𝐴) ∨ (¬ 𝜑𝑋𝐵)) → 𝑋 ∈ V)
93, 8sylbi 218 . . 3 (if-(𝜑, 𝑋𝐴, 𝑋𝐵) → 𝑋 ∈ V)
10 biidd 263 . . . 4 (𝑥 = 𝑋 → (𝜑𝜑))
11 eleq1 2897 . . . 4 (𝑥 = 𝑋 → (𝑥𝐴𝑋𝐴))
12 eleq1 2897 . . . 4 (𝑥 = 𝑋 → (𝑥𝐵𝑋𝐵))
1310, 11, 12ifpbi123d 1069 . . 3 (𝑥 = 𝑋 → (if-(𝜑, 𝑥𝐴, 𝑥𝐵) ↔ if-(𝜑, 𝑋𝐴, 𝑋𝐵)))
149, 13elab3 3671 . 2 (𝑋 ∈ {𝑥 ∣ if-(𝜑, 𝑥𝐴, 𝑥𝐵)} ↔ if-(𝜑, 𝑋𝐴, 𝑋𝐵))
152, 14bitri 276 1 (𝑋 ∈ if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝑋𝐴, 𝑋𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wo 841  if-wif 1054   = wceq 1528  wcel 2105  {cab 2796  Vcvv 3492  ifcif 4463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ifp 1055  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-if 4464
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator