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 2073 and substitution for class variables df-sbc 3684. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3685. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2818 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2715 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 3684 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 227 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 316 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 [wsb 2072 ∈ wcel 2112 {cab 2714 [wsbc 3683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-clab 2715 df-cleq 2728 df-clel 2809 df-sbc 3684 |
This theorem is referenced by: sbsbc 3687 sbc8g 3691 sbc2or 3692 sbceq1a 3694 sbc5ALT 3712 sbcng 3733 sbcimg 3734 sbcan 3735 sbcor 3736 sbcbig 3737 sbcal 3747 sbcex2 3748 sbcel1v 3753 sbctt 3758 sbcralt 3771 sbcreu 3775 rspsbc 3778 rspesbca 3780 sbcel12 4309 sbceqg 4310 csbif 4482 rexreusng 4581 sbcbr123 5093 opelopabsb 5396 csbopab 5421 csbopabgALT 5422 iota4 6339 csbiota 6351 csbriota 7164 onminex 7564 findes 7658 nn0ind-raph 12242 uzind4s 12469 nn0min 30808 sbcrexgOLD 40251 |
Copyright terms: Public domain | W3C validator |