| 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 2065 and substitution for class variables df-sbc 3789. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3790. (Contributed by NM, 31-Dec-2016.) |
| Ref | Expression |
|---|---|
| dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 2829 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
| 2 | df-clab 2715 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
| 3 | df-sbc 3789 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
| 4 | 3 | bicomi 224 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
| 5 | 1, 2, 4 | 3bitr3g 313 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 [wsb 2064 ∈ wcel 2108 {cab 2714 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: sbsbc 3792 sbc8g 3796 sbc2or 3797 sbceq1a 3799 sbc5ALT 3817 sbcng 3836 sbcimg 3837 sbcan 3838 sbcor 3839 sbcbig 3840 sbcim1 3842 sbcal 3849 sbcex2 3850 sbcel1v 3856 sbctt 3860 sbcralt 3872 sbcreu 3876 rspsbc 3879 rspesbca 3881 sbcel12 4411 sbceqg 4412 csbif 4583 rexreusng 4679 sbcbr123 5197 opelopabsb 5535 csbopab 5560 csbopabgALT 5561 iota4 6542 csbiota 6554 csbriota 7403 onminex 7822 findes 7922 nn0ind-raph 12718 uzind4s 12950 nn0min 32822 sbcrexgOLD 42796 |
| Copyright terms: Public domain | W3C validator |