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 1868 and substitution for class variables df-sbc 3403. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3404. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2676 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2597 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 3403 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 213 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 301 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 [wsb 1867 ∈ wcel 1977 {cab 2596 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: sbsbc 3406 sbc8g 3410 sbc2or 3411 sbceq1a 3413 sbc5 3427 sbcng 3443 sbcimg 3444 sbcan 3445 sbcor 3446 sbcbig 3447 sbcal 3452 sbcex2 3453 sbcel1v 3462 sbctt 3467 sbcralt 3477 sbcreu 3482 rspsbc 3484 rspesbca 3486 sbcel12 3935 sbceqg 3936 csbif 4088 sbcbr123 4636 opelopabsb 4910 csbopab 4932 csbopabgALT 4933 iota4 5786 csbiota 5797 csbriota 6523 onminex 6899 findes 6988 nn0ind-raph 11353 uzind4s 11624 nn0min 28954 sbcrexgOLD 36367 sbcangOLD 37760 sbcorgOLD 37761 sbcalgOLD 37773 sbcexgOLD 37774 sbcel12gOLD 37775 sbcel1gvOLD 38116 |
Copyright terms: Public domain | W3C validator |