![]() |
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 2049 and substitution for class variables df-sbc 3586. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3587. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2837 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2757 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 3586 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 214 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 302 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1630 [wsb 2048 ∈ wcel 2144 {cab 2756 [wsbc 3585 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1852 df-clab 2757 df-cleq 2763 df-clel 2766 df-sbc 3586 |
This theorem is referenced by: sbsbc 3589 sbc8g 3593 sbc2or 3594 sbceq1a 3596 sbc5 3610 sbcng 3626 sbcimg 3627 sbcan 3628 sbcor 3629 sbcbig 3630 sbcal 3635 sbcex2 3636 sbcel1v 3644 sbctt 3648 sbcralt 3658 sbcreu 3662 rspsbc 3665 rspesbca 3667 sbcel12 4125 sbceqg 4126 csbif 4275 sbcbr123 4838 opelopabsb 5118 csbopab 5141 csbopabgALT 5142 iota4 6012 csbiota 6024 csbriota 6765 onminex 7153 findes 7242 nn0ind-raph 11678 uzind4s 11949 nn0min 29901 sbcrexgOLD 37868 sbcangOLD 39258 sbcorgOLD 39259 sbcalgOLD 39271 sbcexgOLD 39272 sbcel12gOLD 39273 sbcel1gvOLD 39610 |
Copyright terms: Public domain | W3C validator |