|   | 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 2064 and df-sbc 3788 are equivalent when the class term 𝐴 in df-sbc 3788 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2064 for proofs involving df-sbc 3788. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) | 
| Ref | Expression | 
|---|---|
| sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqid 2736 | . 2 ⊢ 𝑦 = 𝑦 | |
| 2 | dfsbcq2 3790 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 [wsb 2063 [wsbc 3787 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-clab 2714 df-cleq 2728 df-clel 2815 df-sbc 3788 | 
| This theorem is referenced by: spsbc 3800 sbcid 3804 sbccow 3810 sbcco 3813 sbcco2 3814 sbcie2g 3828 eqsbc1 3834 sbcralt 3871 cbvralcsf 3940 cbvreucsf 3942 cbvrabcsf 3943 sbnfc2 4438 csbab 4439 csbie2df 4442 2nreu 4443 frpoins2fg 6364 wfis2fgOLD 6377 isarep1OLD 6656 tfindes 7885 tfinds2 7886 frins2f 9794 iuninc 32574 suppss2f 32649 fmptdF 32667 disjdsct 32713 esumpfinvalf 34078 measiuns 34219 bnj580 34928 bnj985v 34968 bnj985 34969 xpab 35727 setinds2f 35781 bj-sbeq 36903 bj-sbel1 36907 bj-snsetex 36965 poimirlem25 37653 poimirlem26 37654 fdc1 37754 exlimddvfi 38130 frege52b 43907 frege58c 43939 pm13.194 44436 pm14.12 44445 sbiota1 44458 onfrALTlem1 44573 onfrALTlem1VD 44915 disjinfi 45202 ellimcabssub0 45637 2reu8i 47130 ich2exprop 47463 ichnreuop 47464 ichreuopeq 47465 | 
| Copyright terms: Public domain | W3C validator |