Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfsbcq2 | Structured version Visualization version GIF version |
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb 2066 and substitution for class variables df-sbc 3772. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3773. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2900 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2800 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 3772 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 226 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 315 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 [wsb 2065 ∈ wcel 2110 {cab 2799 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbsbc 3775 sbc8g 3779 sbc2or 3780 sbceq1a 3782 sbc5 3799 sbcng 3818 sbcimg 3819 sbcan 3820 sbcor 3821 sbcbig 3822 sbcal 3832 sbcex2 3833 sbcel1v 3838 sbcel1vOLD 3839 sbctt 3843 sbcralt 3854 sbcreu 3858 rspsbc 3861 rspesbca 3863 sbcel12 4359 sbceqg 4360 csbif 4521 rexreusng 4610 sbcbr123 5112 opelopabsb 5409 csbopab 5434 csbopabgALT 5435 iota4 6330 csbiota 6342 csbriota 7123 onminex 7516 findes 7606 nn0ind-raph 12076 uzind4s 12302 nn0min 30531 sbcrexgOLD 39375 |
Copyright terms: Public domain | W3C validator |