![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ceqsalv | Structured version 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 1674 |
. 2
![]() ![]() ![]() ![]() | |
2 | ceqsalv.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | ceqsalv.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | ceqsal 3097 |
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-ext 2430 |
This theorem depends on definitions: df-bi 185 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-v 3072 |
This theorem is referenced by: ralxpxfr2d 3183 clel2 3195 clel4 3198 reu8 3254 frsn 5009 raliunxp 5079 fv3 5804 funimass4 5843 marypha2lem3 7790 kmlem12 8433 fpwwe2lem12 8911 vdwmc2 14144 itg2leub 21330 nmoubi 24309 choc0 24866 nmopub 25449 nmfnleub 25466 heibor1lem 28848 |
Copyright terms: Public domain | W3C validator |