![]() |
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 3777. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3778. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2819 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2708 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 3777 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 223 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 312 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 [wsb 2065 ∈ wcel 2104 {cab 2707 [wsbc 3776 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1780 df-clab 2708 df-cleq 2722 df-clel 2808 df-sbc 3777 |
This theorem is referenced by: sbsbc 3780 sbc8g 3784 sbc2or 3785 sbceq1a 3787 sbc5ALT 3805 sbcng 3826 sbcimg 3827 sbcan 3828 sbcor 3829 sbcbig 3830 sbcim1 3832 sbcal 3840 sbcex2 3841 sbcel1v 3847 sbctt 3852 sbcralt 3865 sbcreu 3869 rspsbc 3872 rspesbca 3874 sbcel12 4407 sbceqg 4408 csbif 4584 rexreusng 4682 sbcbr123 5201 opelopabsb 5529 csbopab 5554 csbopabgALT 5555 iota4 6523 csbiota 6535 csbriota 7383 onminex 7792 findes 7895 nn0ind-raph 12666 uzind4s 12896 nn0min 32293 sbcrexgOLD 41825 |
Copyright terms: Public domain | W3C validator |