![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcvf | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcvf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2602 |
. 2
![]() ![]() ![]() ![]() | |
3 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | dvelimc 2624 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-cleq 2454 df-clel 2457 df-nfc 2591 |
This theorem is referenced by: nfcvf2 2626 nfrald 2784 ralcom2 2966 nfreud 2974 nfrmod 2975 nfrmo 2977 nfdisj 4398 nfcvb 4643 nfiotad 5567 nfriotad 6284 nfixp 7566 axextnd 9041 axrepndlem2 9043 axrepnd 9044 axunndlem1 9045 axunnd 9046 axpowndlem2 9048 axpowndlem4 9050 axregndlem2 9053 axregnd 9054 axinfndlem1 9055 axinfnd 9056 axacndlem4 9060 axacndlem5 9061 axacnd 9062 axextdist 30494 bj-nfcsym 31538 |
Copyright terms: Public domain | W3C validator |