![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > sbcg | Structured version Unicode version |
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3353. (Contributed by Alan Sare, 10-Nov-2012.) |
Ref | Expression |
---|---|
sbcg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1674 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sbcgf 3353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-v 3067 df-sbc 3282 |
This theorem is referenced by: sbcabel 3370 csbuni 4214 csbunigOLD 4215 csbxp 5013 csbxpgOLD 5014 sbcfung 5536 f1od2 26155 sbtru 29046 sbfal 29047 fmptsnd 30857 trsbc 31544 csbxpgVD 31927 csbunigVD 31931 bnj89 32007 bnj525 32027 bnj1128 32278 cdlemk40 34864 cdlemkid3N 34880 cdlemkid4 34881 |
Copyright terms: Public domain | W3C validator |