Mathbox for Wolf Lammen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-dfrabf Structured version   Visualization version   GIF version

Theorem wl-dfrabf 35048
 Description: Alternate definition of restricted class abstraction (df-wl-rab 35044), when 𝑥 is not free in 𝐴. (Contributed by Wolf Lammen, 29-May-2023.)
Assertion
Ref Expression
wl-dfrabf (𝑥𝐴 → {𝑥 : 𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)})

Proof of Theorem wl-dfrabf
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wl-dfrabsb 35045 . 2 {𝑥 : 𝐴𝜑} = {𝑦 ∣ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)}
2 clelsb3 2917 . . . . . 6 ([𝑧 / 𝑦]𝑦𝐴𝑧𝐴)
3 nfnfc1 2958 . . . . . . 7 𝑥𝑥𝐴
4 id 22 . . . . . . 7 (𝑥𝐴𝑥𝐴)
53, 4wl-clelsb3df 35047 . . . . . 6 (𝑥𝐴 → ([𝑧 / 𝑥]𝑥𝐴𝑧𝐴))
62, 5bitr4id 293 . . . . 5 (𝑥𝐴 → ([𝑧 / 𝑦]𝑦𝐴 ↔ [𝑧 / 𝑥]𝑥𝐴))
7 sbco2vv 2105 . . . . . 6 ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
87a1i 11 . . . . 5 (𝑥𝐴 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
96, 8anbi12d 633 . . . 4 (𝑥𝐴 → (([𝑧 / 𝑦]𝑦𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)))
10 df-clab 2777 . . . . 5 (𝑧 ∈ {𝑦 ∣ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ [𝑧 / 𝑦](𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑))
11 sban 2085 . . . . 5 ([𝑧 / 𝑦](𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑦]𝑦𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑))
1210, 11bitri 278 . . . 4 (𝑧 ∈ {𝑦 ∣ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ ([𝑧 / 𝑦]𝑦𝐴 ∧ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑))
13 df-clab 2777 . . . . 5 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ [𝑧 / 𝑥](𝑥𝐴𝜑))
14 sban 2085 . . . . 5 ([𝑧 / 𝑥](𝑥𝐴𝜑) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑))
1513, 14bitri 278 . . . 4 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑))
169, 12, 153bitr4g 317 . . 3 (𝑥𝐴 → (𝑧 ∈ {𝑦 ∣ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)}))
1716eqrdv 2796 . 2 (𝑥𝐴 → {𝑦 ∣ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)} = {𝑥 ∣ (𝑥𝐴𝜑)})
181, 17syl5eq 2845 1 (𝑥𝐴 → {𝑥 : 𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  [wsb 2069   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  {wl-crab 35019 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-wl-rab 35044 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator