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 2075 and df-sbc 3681 are equivalent when the class term 𝐴 in df-sbc 3681 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2075 for proofs involving df-sbc 3681. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 3683 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 [wsb 2074 [wsbc 3680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-clab 2717 df-cleq 2730 df-clel 2811 df-sbc 3681 |
This theorem is referenced by: spsbc 3693 sbcid 3697 sbccow 3703 sbcco 3706 sbcco2 3707 sbcie2g 3721 eqsbc3 3727 sbcralt 3763 cbvralcsf 3832 cbvreucsf 3834 cbvrabcsf 3835 sbnfc2 4326 csbab 4327 csbie2df 4330 2nreu 4331 wfis2fg 6166 isarep1 6427 tfindes 7598 tfinds2 7599 iuninc 30476 suppss2f 30550 fmptdF 30570 disjdsct 30612 esumpfinvalf 31616 measiuns 31757 bnj580 32466 bnj985v 32506 bnj985 32507 xpab 33252 setinds2f 33331 frpoins2fg 33389 frins2fg 33399 bj-sbeq 34732 bj-sbel1 34736 bj-snsetex 34798 poimirlem25 35447 poimirlem26 35448 fdc1 35549 exlimddvfi 35925 frege52b 41065 frege58c 41097 pm13.194 41590 pm14.12 41599 sbiota1 41612 onfrALTlem1 41728 onfrALTlem1VD 42070 disjinfi 42291 ellimcabssub0 42722 2reu8i 44167 ich2exprop 44486 ichnreuop 44487 ichreuopeq 44488 |
Copyright terms: Public domain | W3C validator |