![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbsbc | Structured version Visualization version GIF version |
Description: Show that df-sb 2067 and df-sbc 3778 are equivalent when the class term 𝐴 in df-sbc 3778 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2067 for proofs involving df-sbc 3778. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2731 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 3780 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2066 [wsbc 3777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-clab 2709 df-cleq 2723 df-clel 2809 df-sbc 3778 |
This theorem is referenced by: spsbc 3790 sbcid 3794 sbccow 3800 sbcco 3803 sbcco2 3804 sbcie2g 3819 eqsbc1 3826 sbcralt 3866 cbvralcsf 3938 cbvreucsf 3940 cbvrabcsf 3941 sbnfc2 4436 csbab 4437 csbie2df 4440 2nreu 4441 frpoins2fg 6345 wfis2fgOLD 6358 isarep1OLD 6638 tfindes 7856 tfinds2 7857 frins2f 9754 iuninc 32225 suppss2f 32296 fmptdF 32314 disjdsct 32357 esumpfinvalf 33538 measiuns 33679 bnj580 34388 bnj985v 34428 bnj985 34429 xpab 35165 setinds2f 35221 bj-sbeq 36245 bj-sbel1 36249 bj-snsetex 36308 poimirlem25 36977 poimirlem26 36978 fdc1 37078 exlimddvfi 37454 frege52b 43103 frege58c 43135 pm13.194 43634 pm14.12 43643 sbiota1 43656 onfrALTlem1 43772 onfrALTlem1VD 44114 disjinfi 44350 ellimcabssub0 44792 2reu8i 46280 ich2exprop 46598 ichnreuop 46599 ichreuopeq 46600 |
Copyright terms: Public domain | W3C validator |