New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ceqsalv | Unicode version |
Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
ceqsalv.1 | |
ceqsalv.2 |
Ref | Expression |
---|---|
ceqsalv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 | |
2 | ceqsalv.1 | . 2 | |
3 | ceqsalv.2 | . 2 | |
4 | 1, 2, 3 | ceqsal 2884 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wal 1540 wceq 1642 wcel 1710 cvv 2859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-v 2861 |
This theorem is referenced by: clel2 2975 clel4 2978 reu8 3032 eqpw1 4162 pw111 4170 ssrelk 4211 eqrelk 4212 elp6 4263 sikexlem 4295 insklem 4304 nnadjoin 4520 nnadjoinpw 4521 nnpweq 4523 tfinnn 4534 raliunxp 4823 ssopr 4846 intirr 5029 fv3 5341 funimass4 5368 dfnnc3 5885 spacind 6287 |
Copyright terms: Public domain | W3C validator |