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 2069 and df-sbc 3718 are equivalent when the class term 𝐴 in df-sbc 3718 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2069 for proofs involving df-sbc 3718. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2739 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 3720 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2068 [wsbc 3717 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-clab 2717 df-cleq 2731 df-clel 2817 df-sbc 3718 |
This theorem is referenced by: spsbc 3730 sbcid 3734 sbccow 3740 sbcco 3743 sbcco2 3744 sbcie2g 3759 eqsbc1 3766 sbcralt 3806 cbvralcsf 3878 cbvreucsf 3880 cbvrabcsf 3881 sbnfc2 4371 csbab 4372 csbie2df 4375 2nreu 4376 frpoins2fg 6251 wfis2fgOLD 6264 isarep1OLD 6531 tfindes 7718 tfinds2 7719 frins2f 9520 iuninc 30909 suppss2f 30983 fmptdF 31002 disjdsct 31044 esumpfinvalf 32053 measiuns 32194 bnj580 32902 bnj985v 32942 bnj985 32943 xpab 33686 setinds2f 33764 bj-sbeq 35095 bj-sbel1 35099 bj-snsetex 35162 poimirlem25 35811 poimirlem26 35812 fdc1 35913 exlimddvfi 36289 frege52b 41504 frege58c 41536 pm13.194 42037 pm14.12 42046 sbiota1 42059 onfrALTlem1 42175 onfrALTlem1VD 42517 disjinfi 42738 ellimcabssub0 43165 2reu8i 44616 ich2exprop 44934 ichnreuop 44935 ichreuopeq 44936 |
Copyright terms: Public domain | W3C validator |